YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { #equal(x, y) -> #eq(x, y) , eratos(::(x, xs)) -> ::(x, eratos(filter(x, xs))) , eratos(nil()) -> nil() , filter(p, ::(x, xs)) -> filter'(#equal(#mod(x, p), #0()), x, filter(p, xs)) , filter(p, nil()) -> nil() , #mod(x, y) -> #sub(x, #mult(y, #div(x, y))) , filter'(#true(), x, xs) -> xs , filter'(#false(), x, xs) -> ::(x, xs) } Weak Trs: { #eq(::(x_1, x_2), ::(y_1, y_2)) -> #and(#eq(x_1, y_1), #eq(x_2, y_2)) , #eq(::(x_1, x_2), nil()) -> #false() , #eq(nil(), ::(y_1, y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(y)) -> #false() , #eq(#0(), #neg(y)) -> #false() , #eq(#0(), #pos(y)) -> #false() , #eq(#s(x), #0()) -> #false() , #eq(#s(x), #s(y)) -> #eq(x, y) , #eq(#neg(x), #0()) -> #false() , #eq(#neg(x), #neg(y)) -> #eq(x, y) , #eq(#neg(x), #pos(y)) -> #false() , #eq(#pos(x), #0()) -> #false() , #eq(#pos(x), #neg(y)) -> #false() , #eq(#pos(x), #pos(y)) -> #eq(x, y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(y)) -> #0() , #div(#0(), #pos(y)) -> #0() , #div(#neg(x), #0()) -> #divByZero() , #div(#neg(x), #neg(y)) -> #positive(#natdiv(x, y)) , #div(#neg(x), #pos(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #0()) -> #divByZero() , #div(#pos(x), #neg(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #pos(y)) -> #positive(#natdiv(x, y)) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(y)) -> #0() , #mult(#0(), #pos(y)) -> #0() , #mult(#neg(x), #0()) -> #0() , #mult(#neg(x), #neg(y)) -> #pos(#natmult(x, y)) , #mult(#neg(x), #pos(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #0()) -> #0() , #mult(#pos(x), #neg(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #pos(y)) -> #pos(#natmult(x, y)) , #sub(x, #0()) -> x , #sub(x, #neg(y)) -> #add(x, #pos(y)) , #sub(x, #pos(y)) -> #add(x, #neg(y)) , #add(#0(), y) -> y , #add(#neg(#s(#0())), y) -> #pred(y) , #add(#neg(#s(#s(x))), y) -> #pred(#add(#pos(#s(x)), y)) , #add(#pos(#s(#0())), y) -> #succ(y) , #add(#pos(#s(#s(x))), y) -> #succ(#add(#pos(#s(x)), y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(x))) -> #neg(#s(#s(x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) , #succ(#pos(#s(x))) -> #pos(#s(#s(x))) , #and(#true(), #true()) -> #true() , #and(#true(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#false(), #false()) -> #false() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(y)) -> #0() , #natdiv(#s(x), #0()) -> #divByZero() , #natdiv(#s(x), #s(y)) -> #natdiv'(#divsub(x, y), #s(y)) , #natdiv(#underflow(), y) -> #0() , #positive(#0()) -> #0() , #positive(#s(x)) -> #pos(#s(x)) , #positive(#neg(x)) -> #neg(x) , #positive(#pos(x)) -> #pos(x) , #negative(#0()) -> #0() , #negative(#s(x)) -> #neg(#s(x)) , #negative(#neg(x)) -> #pos(x) , #negative(#pos(x)) -> #neg(x) , #natmult(#0(), y) -> #0() , #natmult(#s(x), y) -> #natadd(y, #natmult(x, y)) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(y)) -> #underflow() , #divsub(#s(x), #0()) -> #s(x) , #divsub(#s(x), #s(y)) -> #divsub(x, y) , #natdiv'(#0(), y) -> #s(#0()) , #natdiv'(#s(x), y) -> #s(#natdiv(#s(x), y)) , #natdiv'(#underflow(), y) -> #0() , #natadd(#0(), y) -> y , #natadd(#s(x), y) -> #s(#natadd(x, y)) , #natsub(#0(), #0()) -> #0() , #natsub(#0(), #s(y)) -> #0() , #natsub(#s(x), #0()) -> #s(x) , #natsub(#s(x), #s(y)) -> #natsub(x, y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We add following dependency tuples: Strict DPs: { #equal^#(x, y) -> c_1(#eq^#(x, y)) , eratos^#(::(x, xs)) -> c_2(eratos^#(filter(x, xs)), filter^#(x, xs)) , eratos^#(nil()) -> c_3() , filter^#(p, ::(x, xs)) -> c_4(filter'^#(#equal(#mod(x, p), #0()), x, filter(p, xs)), #equal^#(#mod(x, p), #0()), #mod^#(x, p), filter^#(p, xs)) , filter^#(p, nil()) -> c_5() , filter'^#(#true(), x, xs) -> c_7() , filter'^#(#false(), x, xs) -> c_8() , #mod^#(x, y) -> c_6(#sub^#(x, #mult(y, #div(x, y))), #mult^#(y, #div(x, y)), #div^#(x, y)) } Weak DPs: { #eq^#(::(x_1, x_2), ::(y_1, y_2)) -> c_9(#and^#(#eq(x_1, y_1), #eq(x_2, y_2)), #eq^#(x_1, y_1), #eq^#(x_2, y_2)) , #eq^#(::(x_1, x_2), nil()) -> c_10() , #eq^#(nil(), ::(y_1, y_2)) -> c_11() , #eq^#(nil(), nil()) -> c_12() , #eq^#(#0(), #0()) -> c_13() , #eq^#(#0(), #s(y)) -> c_14() , #eq^#(#0(), #neg(y)) -> c_15() , #eq^#(#0(), #pos(y)) -> c_16() , #eq^#(#s(x), #0()) -> c_17() , #eq^#(#s(x), #s(y)) -> c_18(#eq^#(x, y)) , #eq^#(#neg(x), #0()) -> c_19() , #eq^#(#neg(x), #neg(y)) -> c_20(#eq^#(x, y)) , #eq^#(#neg(x), #pos(y)) -> c_21() , #eq^#(#pos(x), #0()) -> c_22() , #eq^#(#pos(x), #neg(y)) -> c_23() , #eq^#(#pos(x), #pos(y)) -> c_24(#eq^#(x, y)) , #sub^#(x, #0()) -> c_43() , #sub^#(x, #neg(y)) -> c_44(#add^#(x, #pos(y))) , #sub^#(x, #pos(y)) -> c_45(#add^#(x, #neg(y))) , #mult^#(#0(), #0()) -> c_34() , #mult^#(#0(), #neg(y)) -> c_35() , #mult^#(#0(), #pos(y)) -> c_36() , #mult^#(#neg(x), #0()) -> c_37() , #mult^#(#neg(x), #neg(y)) -> c_38(#natmult^#(x, y)) , #mult^#(#neg(x), #pos(y)) -> c_39(#natmult^#(x, y)) , #mult^#(#pos(x), #0()) -> c_40() , #mult^#(#pos(x), #neg(y)) -> c_41(#natmult^#(x, y)) , #mult^#(#pos(x), #pos(y)) -> c_42(#natmult^#(x, y)) , #div^#(#0(), #0()) -> c_25() , #div^#(#0(), #neg(y)) -> c_26() , #div^#(#0(), #pos(y)) -> c_27() , #div^#(#neg(x), #0()) -> c_28() , #div^#(#neg(x), #neg(y)) -> c_29(#positive^#(#natdiv(x, y)), #natdiv^#(x, y)) , #div^#(#neg(x), #pos(y)) -> c_30(#negative^#(#natdiv(x, y)), #natdiv^#(x, y)) , #div^#(#pos(x), #0()) -> c_31() , #div^#(#pos(x), #neg(y)) -> c_32(#negative^#(#natdiv(x, y)), #natdiv^#(x, y)) , #div^#(#pos(x), #pos(y)) -> c_33(#positive^#(#natdiv(x, y)), #natdiv^#(x, y)) , #and^#(#true(), #true()) -> c_59() , #and^#(#true(), #false()) -> c_60() , #and^#(#false(), #true()) -> c_61() , #and^#(#false(), #false()) -> c_62() , #positive^#(#0()) -> c_68() , #positive^#(#s(x)) -> c_69() , #positive^#(#neg(x)) -> c_70() , #positive^#(#pos(x)) -> c_71() , #natdiv^#(#0(), #0()) -> c_63() , #natdiv^#(#0(), #s(y)) -> c_64() , #natdiv^#(#s(x), #0()) -> c_65() , #natdiv^#(#s(x), #s(y)) -> c_66(#natdiv'^#(#divsub(x, y), #s(y)), #divsub^#(x, y)) , #natdiv^#(#underflow(), y) -> c_67() , #negative^#(#0()) -> c_72() , #negative^#(#s(x)) -> c_73() , #negative^#(#neg(x)) -> c_74() , #negative^#(#pos(x)) -> c_75() , #natmult^#(#0(), y) -> c_76() , #natmult^#(#s(x), y) -> c_77(#natadd^#(y, #natmult(x, y)), #natmult^#(x, y)) , #add^#(#0(), y) -> c_46() , #add^#(#neg(#s(#0())), y) -> c_47(#pred^#(y)) , #add^#(#neg(#s(#s(x))), y) -> c_48(#pred^#(#add(#pos(#s(x)), y)), #add^#(#pos(#s(x)), y)) , #add^#(#pos(#s(#0())), y) -> c_49(#succ^#(y)) , #add^#(#pos(#s(#s(x))), y) -> c_50(#succ^#(#add(#pos(#s(x)), y)), #add^#(#pos(#s(x)), y)) , #pred^#(#0()) -> c_51() , #pred^#(#neg(#s(x))) -> c_52() , #pred^#(#pos(#s(#0()))) -> c_53() , #pred^#(#pos(#s(#s(x)))) -> c_54() , #succ^#(#0()) -> c_55() , #succ^#(#neg(#s(#0()))) -> c_56() , #succ^#(#neg(#s(#s(x)))) -> c_57() , #succ^#(#pos(#s(x))) -> c_58() , #natdiv'^#(#0(), y) -> c_82() , #natdiv'^#(#s(x), y) -> c_83(#natdiv^#(#s(x), y)) , #natdiv'^#(#underflow(), y) -> c_84() , #divsub^#(#0(), #0()) -> c_78() , #divsub^#(#0(), #s(y)) -> c_79() , #divsub^#(#s(x), #0()) -> c_80() , #divsub^#(#s(x), #s(y)) -> c_81(#divsub^#(x, y)) , #natadd^#(#0(), y) -> c_85() , #natadd^#(#s(x), y) -> c_86(#natadd^#(x, y)) , #natsub^#(#0(), #0()) -> c_87() , #natsub^#(#0(), #s(y)) -> c_88() , #natsub^#(#s(x), #0()) -> c_89() , #natsub^#(#s(x), #s(y)) -> c_90(#natsub^#(x, y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { #equal^#(x, y) -> c_1(#eq^#(x, y)) , eratos^#(::(x, xs)) -> c_2(eratos^#(filter(x, xs)), filter^#(x, xs)) , eratos^#(nil()) -> c_3() , filter^#(p, ::(x, xs)) -> c_4(filter'^#(#equal(#mod(x, p), #0()), x, filter(p, xs)), #equal^#(#mod(x, p), #0()), #mod^#(x, p), filter^#(p, xs)) , filter^#(p, nil()) -> c_5() , filter'^#(#true(), x, xs) -> c_7() , filter'^#(#false(), x, xs) -> c_8() , #mod^#(x, y) -> c_6(#sub^#(x, #mult(y, #div(x, y))), #mult^#(y, #div(x, y)), #div^#(x, y)) } Weak DPs: { #eq^#(::(x_1, x_2), ::(y_1, y_2)) -> c_9(#and^#(#eq(x_1, y_1), #eq(x_2, y_2)), #eq^#(x_1, y_1), #eq^#(x_2, y_2)) , #eq^#(::(x_1, x_2), nil()) -> c_10() , #eq^#(nil(), ::(y_1, y_2)) -> c_11() , #eq^#(nil(), nil()) -> c_12() , #eq^#(#0(), #0()) -> c_13() , #eq^#(#0(), #s(y)) -> c_14() , #eq^#(#0(), #neg(y)) -> c_15() , #eq^#(#0(), #pos(y)) -> c_16() , #eq^#(#s(x), #0()) -> c_17() , #eq^#(#s(x), #s(y)) -> c_18(#eq^#(x, y)) , #eq^#(#neg(x), #0()) -> c_19() , #eq^#(#neg(x), #neg(y)) -> c_20(#eq^#(x, y)) , #eq^#(#neg(x), #pos(y)) -> c_21() , #eq^#(#pos(x), #0()) -> c_22() , #eq^#(#pos(x), #neg(y)) -> c_23() , #eq^#(#pos(x), #pos(y)) -> c_24(#eq^#(x, y)) , #sub^#(x, #0()) -> c_43() , #sub^#(x, #neg(y)) -> c_44(#add^#(x, #pos(y))) , #sub^#(x, #pos(y)) -> c_45(#add^#(x, #neg(y))) , #mult^#(#0(), #0()) -> c_34() , #mult^#(#0(), #neg(y)) -> c_35() , #mult^#(#0(), #pos(y)) -> c_36() , #mult^#(#neg(x), #0()) -> c_37() , #mult^#(#neg(x), #neg(y)) -> c_38(#natmult^#(x, y)) , #mult^#(#neg(x), #pos(y)) -> c_39(#natmult^#(x, y)) , #mult^#(#pos(x), #0()) -> c_40() , #mult^#(#pos(x), #neg(y)) -> c_41(#natmult^#(x, y)) , #mult^#(#pos(x), #pos(y)) -> c_42(#natmult^#(x, y)) , #div^#(#0(), #0()) -> c_25() , #div^#(#0(), #neg(y)) -> c_26() , #div^#(#0(), #pos(y)) -> c_27() , #div^#(#neg(x), #0()) -> c_28() , #div^#(#neg(x), #neg(y)) -> c_29(#positive^#(#natdiv(x, y)), #natdiv^#(x, y)) , #div^#(#neg(x), #pos(y)) -> c_30(#negative^#(#natdiv(x, y)), #natdiv^#(x, y)) , #div^#(#pos(x), #0()) -> c_31() , #div^#(#pos(x), #neg(y)) -> c_32(#negative^#(#natdiv(x, y)), #natdiv^#(x, y)) , #div^#(#pos(x), #pos(y)) -> c_33(#positive^#(#natdiv(x, y)), #natdiv^#(x, y)) , #and^#(#true(), #true()) -> c_59() , #and^#(#true(), #false()) -> c_60() , #and^#(#false(), #true()) -> c_61() , #and^#(#false(), #false()) -> c_62() , #positive^#(#0()) -> c_68() , #positive^#(#s(x)) -> c_69() , #positive^#(#neg(x)) -> c_70() , #positive^#(#pos(x)) -> c_71() , #natdiv^#(#0(), #0()) -> c_63() , #natdiv^#(#0(), #s(y)) -> c_64() , #natdiv^#(#s(x), #0()) -> c_65() , #natdiv^#(#s(x), #s(y)) -> c_66(#natdiv'^#(#divsub(x, y), #s(y)), #divsub^#(x, y)) , #natdiv^#(#underflow(), y) -> c_67() , #negative^#(#0()) -> c_72() , #negative^#(#s(x)) -> c_73() , #negative^#(#neg(x)) -> c_74() , #negative^#(#pos(x)) -> c_75() , #natmult^#(#0(), y) -> c_76() , #natmult^#(#s(x), y) -> c_77(#natadd^#(y, #natmult(x, y)), #natmult^#(x, y)) , #add^#(#0(), y) -> c_46() , #add^#(#neg(#s(#0())), y) -> c_47(#pred^#(y)) , #add^#(#neg(#s(#s(x))), y) -> c_48(#pred^#(#add(#pos(#s(x)), y)), #add^#(#pos(#s(x)), y)) , #add^#(#pos(#s(#0())), y) -> c_49(#succ^#(y)) , #add^#(#pos(#s(#s(x))), y) -> c_50(#succ^#(#add(#pos(#s(x)), y)), #add^#(#pos(#s(x)), y)) , #pred^#(#0()) -> c_51() , #pred^#(#neg(#s(x))) -> c_52() , #pred^#(#pos(#s(#0()))) -> c_53() , #pred^#(#pos(#s(#s(x)))) -> c_54() , #succ^#(#0()) -> c_55() , #succ^#(#neg(#s(#0()))) -> c_56() , #succ^#(#neg(#s(#s(x)))) -> c_57() , #succ^#(#pos(#s(x))) -> c_58() , #natdiv'^#(#0(), y) -> c_82() , #natdiv'^#(#s(x), y) -> c_83(#natdiv^#(#s(x), y)) , #natdiv'^#(#underflow(), y) -> c_84() , #divsub^#(#0(), #0()) -> c_78() , #divsub^#(#0(), #s(y)) -> c_79() , #divsub^#(#s(x), #0()) -> c_80() , #divsub^#(#s(x), #s(y)) -> c_81(#divsub^#(x, y)) , #natadd^#(#0(), y) -> c_85() , #natadd^#(#s(x), y) -> c_86(#natadd^#(x, y)) , #natsub^#(#0(), #0()) -> c_87() , #natsub^#(#0(), #s(y)) -> c_88() , #natsub^#(#s(x), #0()) -> c_89() , #natsub^#(#s(x), #s(y)) -> c_90(#natsub^#(x, y)) } Weak Trs: { #equal(x, y) -> #eq(x, y) , #eq(::(x_1, x_2), ::(y_1, y_2)) -> #and(#eq(x_1, y_1), #eq(x_2, y_2)) , #eq(::(x_1, x_2), nil()) -> #false() , #eq(nil(), ::(y_1, y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(y)) -> #false() , #eq(#0(), #neg(y)) -> #false() , #eq(#0(), #pos(y)) -> #false() , #eq(#s(x), #0()) -> #false() , #eq(#s(x), #s(y)) -> #eq(x, y) , #eq(#neg(x), #0()) -> #false() , #eq(#neg(x), #neg(y)) -> #eq(x, y) , #eq(#neg(x), #pos(y)) -> #false() , #eq(#pos(x), #0()) -> #false() , #eq(#pos(x), #neg(y)) -> #false() , #eq(#pos(x), #pos(y)) -> #eq(x, y) , eratos(::(x, xs)) -> ::(x, eratos(filter(x, xs))) , eratos(nil()) -> nil() , filter(p, ::(x, xs)) -> filter'(#equal(#mod(x, p), #0()), x, filter(p, xs)) , filter(p, nil()) -> nil() , #mod(x, y) -> #sub(x, #mult(y, #div(x, y))) , filter'(#true(), x, xs) -> xs , filter'(#false(), x, xs) -> ::(x, xs) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(y)) -> #0() , #div(#0(), #pos(y)) -> #0() , #div(#neg(x), #0()) -> #divByZero() , #div(#neg(x), #neg(y)) -> #positive(#natdiv(x, y)) , #div(#neg(x), #pos(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #0()) -> #divByZero() , #div(#pos(x), #neg(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #pos(y)) -> #positive(#natdiv(x, y)) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(y)) -> #0() , #mult(#0(), #pos(y)) -> #0() , #mult(#neg(x), #0()) -> #0() , #mult(#neg(x), #neg(y)) -> #pos(#natmult(x, y)) , #mult(#neg(x), #pos(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #0()) -> #0() , #mult(#pos(x), #neg(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #pos(y)) -> #pos(#natmult(x, y)) , #sub(x, #0()) -> x , #sub(x, #neg(y)) -> #add(x, #pos(y)) , #sub(x, #pos(y)) -> #add(x, #neg(y)) , #add(#0(), y) -> y , #add(#neg(#s(#0())), y) -> #pred(y) , #add(#neg(#s(#s(x))), y) -> #pred(#add(#pos(#s(x)), y)) , #add(#pos(#s(#0())), y) -> #succ(y) , #add(#pos(#s(#s(x))), y) -> #succ(#add(#pos(#s(x)), y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(x))) -> #neg(#s(#s(x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) , #succ(#pos(#s(x))) -> #pos(#s(#s(x))) , #and(#true(), #true()) -> #true() , #and(#true(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#false(), #false()) -> #false() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(y)) -> #0() , #natdiv(#s(x), #0()) -> #divByZero() , #natdiv(#s(x), #s(y)) -> #natdiv'(#divsub(x, y), #s(y)) , #natdiv(#underflow(), y) -> #0() , #positive(#0()) -> #0() , #positive(#s(x)) -> #pos(#s(x)) , #positive(#neg(x)) -> #neg(x) , #positive(#pos(x)) -> #pos(x) , #negative(#0()) -> #0() , #negative(#s(x)) -> #neg(#s(x)) , #negative(#neg(x)) -> #pos(x) , #negative(#pos(x)) -> #neg(x) , #natmult(#0(), y) -> #0() , #natmult(#s(x), y) -> #natadd(y, #natmult(x, y)) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(y)) -> #underflow() , #divsub(#s(x), #0()) -> #s(x) , #divsub(#s(x), #s(y)) -> #divsub(x, y) , #natdiv'(#0(), y) -> #s(#0()) , #natdiv'(#s(x), y) -> #s(#natdiv(#s(x), y)) , #natdiv'(#underflow(), y) -> #0() , #natadd(#0(), y) -> y , #natadd(#s(x), y) -> #s(#natadd(x, y)) , #natsub(#0(), #0()) -> #0() , #natsub(#0(), #s(y)) -> #0() , #natsub(#s(x), #0()) -> #s(x) , #natsub(#s(x), #s(y)) -> #natsub(x, y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {1,3,5,6,7,8} by applications of Pre({1,3,5,6,7,8}) = {2,4}. Here rules are labeled as follows: DPs: { 1: #equal^#(x, y) -> c_1(#eq^#(x, y)) , 2: eratos^#(::(x, xs)) -> c_2(eratos^#(filter(x, xs)), filter^#(x, xs)) , 3: eratos^#(nil()) -> c_3() , 4: filter^#(p, ::(x, xs)) -> c_4(filter'^#(#equal(#mod(x, p), #0()), x, filter(p, xs)), #equal^#(#mod(x, p), #0()), #mod^#(x, p), filter^#(p, xs)) , 5: filter^#(p, nil()) -> c_5() , 6: filter'^#(#true(), x, xs) -> c_7() , 7: filter'^#(#false(), x, xs) -> c_8() , 8: #mod^#(x, y) -> c_6(#sub^#(x, #mult(y, #div(x, y))), #mult^#(y, #div(x, y)), #div^#(x, y)) , 9: #eq^#(::(x_1, x_2), ::(y_1, y_2)) -> c_9(#and^#(#eq(x_1, y_1), #eq(x_2, y_2)), #eq^#(x_1, y_1), #eq^#(x_2, y_2)) , 10: #eq^#(::(x_1, x_2), nil()) -> c_10() , 11: #eq^#(nil(), ::(y_1, y_2)) -> c_11() , 12: #eq^#(nil(), nil()) -> c_12() , 13: #eq^#(#0(), #0()) -> c_13() , 14: #eq^#(#0(), #s(y)) -> c_14() , 15: #eq^#(#0(), #neg(y)) -> c_15() , 16: #eq^#(#0(), #pos(y)) -> c_16() , 17: #eq^#(#s(x), #0()) -> c_17() , 18: #eq^#(#s(x), #s(y)) -> c_18(#eq^#(x, y)) , 19: #eq^#(#neg(x), #0()) -> c_19() , 20: #eq^#(#neg(x), #neg(y)) -> c_20(#eq^#(x, y)) , 21: #eq^#(#neg(x), #pos(y)) -> c_21() , 22: #eq^#(#pos(x), #0()) -> c_22() , 23: #eq^#(#pos(x), #neg(y)) -> c_23() , 24: #eq^#(#pos(x), #pos(y)) -> c_24(#eq^#(x, y)) , 25: #sub^#(x, #0()) -> c_43() , 26: #sub^#(x, #neg(y)) -> c_44(#add^#(x, #pos(y))) , 27: #sub^#(x, #pos(y)) -> c_45(#add^#(x, #neg(y))) , 28: #mult^#(#0(), #0()) -> c_34() , 29: #mult^#(#0(), #neg(y)) -> c_35() , 30: #mult^#(#0(), #pos(y)) -> c_36() , 31: #mult^#(#neg(x), #0()) -> c_37() , 32: #mult^#(#neg(x), #neg(y)) -> c_38(#natmult^#(x, y)) , 33: #mult^#(#neg(x), #pos(y)) -> c_39(#natmult^#(x, y)) , 34: #mult^#(#pos(x), #0()) -> c_40() , 35: #mult^#(#pos(x), #neg(y)) -> c_41(#natmult^#(x, y)) , 36: #mult^#(#pos(x), #pos(y)) -> c_42(#natmult^#(x, y)) , 37: #div^#(#0(), #0()) -> c_25() , 38: #div^#(#0(), #neg(y)) -> c_26() , 39: #div^#(#0(), #pos(y)) -> c_27() , 40: #div^#(#neg(x), #0()) -> c_28() , 41: #div^#(#neg(x), #neg(y)) -> c_29(#positive^#(#natdiv(x, y)), #natdiv^#(x, y)) , 42: #div^#(#neg(x), #pos(y)) -> c_30(#negative^#(#natdiv(x, y)), #natdiv^#(x, y)) , 43: #div^#(#pos(x), #0()) -> c_31() , 44: #div^#(#pos(x), #neg(y)) -> c_32(#negative^#(#natdiv(x, y)), #natdiv^#(x, y)) , 45: #div^#(#pos(x), #pos(y)) -> c_33(#positive^#(#natdiv(x, y)), #natdiv^#(x, y)) , 46: #and^#(#true(), #true()) -> c_59() , 47: #and^#(#true(), #false()) -> c_60() , 48: #and^#(#false(), #true()) -> c_61() , 49: #and^#(#false(), #false()) -> c_62() , 50: #positive^#(#0()) -> c_68() , 51: #positive^#(#s(x)) -> c_69() , 52: #positive^#(#neg(x)) -> c_70() , 53: #positive^#(#pos(x)) -> c_71() , 54: #natdiv^#(#0(), #0()) -> c_63() , 55: #natdiv^#(#0(), #s(y)) -> c_64() , 56: #natdiv^#(#s(x), #0()) -> c_65() , 57: #natdiv^#(#s(x), #s(y)) -> c_66(#natdiv'^#(#divsub(x, y), #s(y)), #divsub^#(x, y)) , 58: #natdiv^#(#underflow(), y) -> c_67() , 59: #negative^#(#0()) -> c_72() , 60: #negative^#(#s(x)) -> c_73() , 61: #negative^#(#neg(x)) -> c_74() , 62: #negative^#(#pos(x)) -> c_75() , 63: #natmult^#(#0(), y) -> c_76() , 64: #natmult^#(#s(x), y) -> c_77(#natadd^#(y, #natmult(x, y)), #natmult^#(x, y)) , 65: #add^#(#0(), y) -> c_46() , 66: #add^#(#neg(#s(#0())), y) -> c_47(#pred^#(y)) , 67: #add^#(#neg(#s(#s(x))), y) -> c_48(#pred^#(#add(#pos(#s(x)), y)), #add^#(#pos(#s(x)), y)) , 68: #add^#(#pos(#s(#0())), y) -> c_49(#succ^#(y)) , 69: #add^#(#pos(#s(#s(x))), y) -> c_50(#succ^#(#add(#pos(#s(x)), y)), #add^#(#pos(#s(x)), y)) , 70: #pred^#(#0()) -> c_51() , 71: #pred^#(#neg(#s(x))) -> c_52() , 72: #pred^#(#pos(#s(#0()))) -> c_53() , 73: #pred^#(#pos(#s(#s(x)))) -> c_54() , 74: #succ^#(#0()) -> c_55() , 75: #succ^#(#neg(#s(#0()))) -> c_56() , 76: #succ^#(#neg(#s(#s(x)))) -> c_57() , 77: #succ^#(#pos(#s(x))) -> c_58() , 78: #natdiv'^#(#0(), y) -> c_82() , 79: #natdiv'^#(#s(x), y) -> c_83(#natdiv^#(#s(x), y)) , 80: #natdiv'^#(#underflow(), y) -> c_84() , 81: #divsub^#(#0(), #0()) -> c_78() , 82: #divsub^#(#0(), #s(y)) -> c_79() , 83: #divsub^#(#s(x), #0()) -> c_80() , 84: #divsub^#(#s(x), #s(y)) -> c_81(#divsub^#(x, y)) , 85: #natadd^#(#0(), y) -> c_85() , 86: #natadd^#(#s(x), y) -> c_86(#natadd^#(x, y)) , 87: #natsub^#(#0(), #0()) -> c_87() , 88: #natsub^#(#0(), #s(y)) -> c_88() , 89: #natsub^#(#s(x), #0()) -> c_89() , 90: #natsub^#(#s(x), #s(y)) -> c_90(#natsub^#(x, y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(::(x, xs)) -> c_2(eratos^#(filter(x, xs)), filter^#(x, xs)) , filter^#(p, ::(x, xs)) -> c_4(filter'^#(#equal(#mod(x, p), #0()), x, filter(p, xs)), #equal^#(#mod(x, p), #0()), #mod^#(x, p), filter^#(p, xs)) } Weak DPs: { #equal^#(x, y) -> c_1(#eq^#(x, y)) , #eq^#(::(x_1, x_2), ::(y_1, y_2)) -> c_9(#and^#(#eq(x_1, y_1), #eq(x_2, y_2)), #eq^#(x_1, y_1), #eq^#(x_2, y_2)) , #eq^#(::(x_1, x_2), nil()) -> c_10() , #eq^#(nil(), ::(y_1, y_2)) -> c_11() , #eq^#(nil(), nil()) -> c_12() , #eq^#(#0(), #0()) -> c_13() , #eq^#(#0(), #s(y)) -> c_14() , #eq^#(#0(), #neg(y)) -> c_15() , #eq^#(#0(), #pos(y)) -> c_16() , #eq^#(#s(x), #0()) -> c_17() , #eq^#(#s(x), #s(y)) -> c_18(#eq^#(x, y)) , #eq^#(#neg(x), #0()) -> c_19() , #eq^#(#neg(x), #neg(y)) -> c_20(#eq^#(x, y)) , #eq^#(#neg(x), #pos(y)) -> c_21() , #eq^#(#pos(x), #0()) -> c_22() , #eq^#(#pos(x), #neg(y)) -> c_23() , #eq^#(#pos(x), #pos(y)) -> c_24(#eq^#(x, y)) , eratos^#(nil()) -> c_3() , filter^#(p, nil()) -> c_5() , filter'^#(#true(), x, xs) -> c_7() , filter'^#(#false(), x, xs) -> c_8() , #mod^#(x, y) -> c_6(#sub^#(x, #mult(y, #div(x, y))), #mult^#(y, #div(x, y)), #div^#(x, y)) , #sub^#(x, #0()) -> c_43() , #sub^#(x, #neg(y)) -> c_44(#add^#(x, #pos(y))) , #sub^#(x, #pos(y)) -> c_45(#add^#(x, #neg(y))) , #mult^#(#0(), #0()) -> c_34() , #mult^#(#0(), #neg(y)) -> c_35() , #mult^#(#0(), #pos(y)) -> c_36() , #mult^#(#neg(x), #0()) -> c_37() , #mult^#(#neg(x), #neg(y)) -> c_38(#natmult^#(x, y)) , #mult^#(#neg(x), #pos(y)) -> c_39(#natmult^#(x, y)) , #mult^#(#pos(x), #0()) -> c_40() , #mult^#(#pos(x), #neg(y)) -> c_41(#natmult^#(x, y)) , #mult^#(#pos(x), #pos(y)) -> c_42(#natmult^#(x, y)) , #div^#(#0(), #0()) -> c_25() , #div^#(#0(), #neg(y)) -> c_26() , #div^#(#0(), #pos(y)) -> c_27() , #div^#(#neg(x), #0()) -> c_28() , #div^#(#neg(x), #neg(y)) -> c_29(#positive^#(#natdiv(x, y)), #natdiv^#(x, y)) , #div^#(#neg(x), #pos(y)) -> c_30(#negative^#(#natdiv(x, y)), #natdiv^#(x, y)) , #div^#(#pos(x), #0()) -> c_31() , #div^#(#pos(x), #neg(y)) -> c_32(#negative^#(#natdiv(x, y)), #natdiv^#(x, y)) , #div^#(#pos(x), #pos(y)) -> c_33(#positive^#(#natdiv(x, y)), #natdiv^#(x, y)) , #and^#(#true(), #true()) -> c_59() , #and^#(#true(), #false()) -> c_60() , #and^#(#false(), #true()) -> c_61() , #and^#(#false(), #false()) -> c_62() , #positive^#(#0()) -> c_68() , #positive^#(#s(x)) -> c_69() , #positive^#(#neg(x)) -> c_70() , #positive^#(#pos(x)) -> c_71() , #natdiv^#(#0(), #0()) -> c_63() , #natdiv^#(#0(), #s(y)) -> c_64() , #natdiv^#(#s(x), #0()) -> c_65() , #natdiv^#(#s(x), #s(y)) -> c_66(#natdiv'^#(#divsub(x, y), #s(y)), #divsub^#(x, y)) , #natdiv^#(#underflow(), y) -> c_67() , #negative^#(#0()) -> c_72() , #negative^#(#s(x)) -> c_73() , #negative^#(#neg(x)) -> c_74() , #negative^#(#pos(x)) -> c_75() , #natmult^#(#0(), y) -> c_76() , #natmult^#(#s(x), y) -> c_77(#natadd^#(y, #natmult(x, y)), #natmult^#(x, y)) , #add^#(#0(), y) -> c_46() , #add^#(#neg(#s(#0())), y) -> c_47(#pred^#(y)) , #add^#(#neg(#s(#s(x))), y) -> c_48(#pred^#(#add(#pos(#s(x)), y)), #add^#(#pos(#s(x)), y)) , #add^#(#pos(#s(#0())), y) -> c_49(#succ^#(y)) , #add^#(#pos(#s(#s(x))), y) -> c_50(#succ^#(#add(#pos(#s(x)), y)), #add^#(#pos(#s(x)), y)) , #pred^#(#0()) -> c_51() , #pred^#(#neg(#s(x))) -> c_52() , #pred^#(#pos(#s(#0()))) -> c_53() , #pred^#(#pos(#s(#s(x)))) -> c_54() , #succ^#(#0()) -> c_55() , #succ^#(#neg(#s(#0()))) -> c_56() , #succ^#(#neg(#s(#s(x)))) -> c_57() , #succ^#(#pos(#s(x))) -> c_58() , #natdiv'^#(#0(), y) -> c_82() , #natdiv'^#(#s(x), y) -> c_83(#natdiv^#(#s(x), y)) , #natdiv'^#(#underflow(), y) -> c_84() , #divsub^#(#0(), #0()) -> c_78() , #divsub^#(#0(), #s(y)) -> c_79() , #divsub^#(#s(x), #0()) -> c_80() , #divsub^#(#s(x), #s(y)) -> c_81(#divsub^#(x, y)) , #natadd^#(#0(), y) -> c_85() , #natadd^#(#s(x), y) -> c_86(#natadd^#(x, y)) , #natsub^#(#0(), #0()) -> c_87() , #natsub^#(#0(), #s(y)) -> c_88() , #natsub^#(#s(x), #0()) -> c_89() , #natsub^#(#s(x), #s(y)) -> c_90(#natsub^#(x, y)) } Weak Trs: { #equal(x, y) -> #eq(x, y) , #eq(::(x_1, x_2), ::(y_1, y_2)) -> #and(#eq(x_1, y_1), #eq(x_2, y_2)) , #eq(::(x_1, x_2), nil()) -> #false() , #eq(nil(), ::(y_1, y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(y)) -> #false() , #eq(#0(), #neg(y)) -> #false() , #eq(#0(), #pos(y)) -> #false() , #eq(#s(x), #0()) -> #false() , #eq(#s(x), #s(y)) -> #eq(x, y) , #eq(#neg(x), #0()) -> #false() , #eq(#neg(x), #neg(y)) -> #eq(x, y) , #eq(#neg(x), #pos(y)) -> #false() , #eq(#pos(x), #0()) -> #false() , #eq(#pos(x), #neg(y)) -> #false() , #eq(#pos(x), #pos(y)) -> #eq(x, y) , eratos(::(x, xs)) -> ::(x, eratos(filter(x, xs))) , eratos(nil()) -> nil() , filter(p, ::(x, xs)) -> filter'(#equal(#mod(x, p), #0()), x, filter(p, xs)) , filter(p, nil()) -> nil() , #mod(x, y) -> #sub(x, #mult(y, #div(x, y))) , filter'(#true(), x, xs) -> xs , filter'(#false(), x, xs) -> ::(x, xs) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(y)) -> #0() , #div(#0(), #pos(y)) -> #0() , #div(#neg(x), #0()) -> #divByZero() , #div(#neg(x), #neg(y)) -> #positive(#natdiv(x, y)) , #div(#neg(x), #pos(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #0()) -> #divByZero() , #div(#pos(x), #neg(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #pos(y)) -> #positive(#natdiv(x, y)) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(y)) -> #0() , #mult(#0(), #pos(y)) -> #0() , #mult(#neg(x), #0()) -> #0() , #mult(#neg(x), #neg(y)) -> #pos(#natmult(x, y)) , #mult(#neg(x), #pos(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #0()) -> #0() , #mult(#pos(x), #neg(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #pos(y)) -> #pos(#natmult(x, y)) , #sub(x, #0()) -> x , #sub(x, #neg(y)) -> #add(x, #pos(y)) , #sub(x, #pos(y)) -> #add(x, #neg(y)) , #add(#0(), y) -> y , #add(#neg(#s(#0())), y) -> #pred(y) , #add(#neg(#s(#s(x))), y) -> #pred(#add(#pos(#s(x)), y)) , #add(#pos(#s(#0())), y) -> #succ(y) , #add(#pos(#s(#s(x))), y) -> #succ(#add(#pos(#s(x)), y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(x))) -> #neg(#s(#s(x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) , #succ(#pos(#s(x))) -> #pos(#s(#s(x))) , #and(#true(), #true()) -> #true() , #and(#true(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#false(), #false()) -> #false() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(y)) -> #0() , #natdiv(#s(x), #0()) -> #divByZero() , #natdiv(#s(x), #s(y)) -> #natdiv'(#divsub(x, y), #s(y)) , #natdiv(#underflow(), y) -> #0() , #positive(#0()) -> #0() , #positive(#s(x)) -> #pos(#s(x)) , #positive(#neg(x)) -> #neg(x) , #positive(#pos(x)) -> #pos(x) , #negative(#0()) -> #0() , #negative(#s(x)) -> #neg(#s(x)) , #negative(#neg(x)) -> #pos(x) , #negative(#pos(x)) -> #neg(x) , #natmult(#0(), y) -> #0() , #natmult(#s(x), y) -> #natadd(y, #natmult(x, y)) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(y)) -> #underflow() , #divsub(#s(x), #0()) -> #s(x) , #divsub(#s(x), #s(y)) -> #divsub(x, y) , #natdiv'(#0(), y) -> #s(#0()) , #natdiv'(#s(x), y) -> #s(#natdiv(#s(x), y)) , #natdiv'(#underflow(), y) -> #0() , #natadd(#0(), y) -> y , #natadd(#s(x), y) -> #s(#natadd(x, y)) , #natsub(#0(), #0()) -> #0() , #natsub(#0(), #s(y)) -> #0() , #natsub(#s(x), #0()) -> #s(x) , #natsub(#s(x), #s(y)) -> #natsub(x, y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { #equal^#(x, y) -> c_1(#eq^#(x, y)) , #eq^#(::(x_1, x_2), ::(y_1, y_2)) -> c_9(#and^#(#eq(x_1, y_1), #eq(x_2, y_2)), #eq^#(x_1, y_1), #eq^#(x_2, y_2)) , #eq^#(::(x_1, x_2), nil()) -> c_10() , #eq^#(nil(), ::(y_1, y_2)) -> c_11() , #eq^#(nil(), nil()) -> c_12() , #eq^#(#0(), #0()) -> c_13() , #eq^#(#0(), #s(y)) -> c_14() , #eq^#(#0(), #neg(y)) -> c_15() , #eq^#(#0(), #pos(y)) -> c_16() , #eq^#(#s(x), #0()) -> c_17() , #eq^#(#s(x), #s(y)) -> c_18(#eq^#(x, y)) , #eq^#(#neg(x), #0()) -> c_19() , #eq^#(#neg(x), #neg(y)) -> c_20(#eq^#(x, y)) , #eq^#(#neg(x), #pos(y)) -> c_21() , #eq^#(#pos(x), #0()) -> c_22() , #eq^#(#pos(x), #neg(y)) -> c_23() , #eq^#(#pos(x), #pos(y)) -> c_24(#eq^#(x, y)) , eratos^#(nil()) -> c_3() , filter^#(p, nil()) -> c_5() , filter'^#(#true(), x, xs) -> c_7() , filter'^#(#false(), x, xs) -> c_8() , #mod^#(x, y) -> c_6(#sub^#(x, #mult(y, #div(x, y))), #mult^#(y, #div(x, y)), #div^#(x, y)) , #sub^#(x, #0()) -> c_43() , #sub^#(x, #neg(y)) -> c_44(#add^#(x, #pos(y))) , #sub^#(x, #pos(y)) -> c_45(#add^#(x, #neg(y))) , #mult^#(#0(), #0()) -> c_34() , #mult^#(#0(), #neg(y)) -> c_35() , #mult^#(#0(), #pos(y)) -> c_36() , #mult^#(#neg(x), #0()) -> c_37() , #mult^#(#neg(x), #neg(y)) -> c_38(#natmult^#(x, y)) , #mult^#(#neg(x), #pos(y)) -> c_39(#natmult^#(x, y)) , #mult^#(#pos(x), #0()) -> c_40() , #mult^#(#pos(x), #neg(y)) -> c_41(#natmult^#(x, y)) , #mult^#(#pos(x), #pos(y)) -> c_42(#natmult^#(x, y)) , #div^#(#0(), #0()) -> c_25() , #div^#(#0(), #neg(y)) -> c_26() , #div^#(#0(), #pos(y)) -> c_27() , #div^#(#neg(x), #0()) -> c_28() , #div^#(#neg(x), #neg(y)) -> c_29(#positive^#(#natdiv(x, y)), #natdiv^#(x, y)) , #div^#(#neg(x), #pos(y)) -> c_30(#negative^#(#natdiv(x, y)), #natdiv^#(x, y)) , #div^#(#pos(x), #0()) -> c_31() , #div^#(#pos(x), #neg(y)) -> c_32(#negative^#(#natdiv(x, y)), #natdiv^#(x, y)) , #div^#(#pos(x), #pos(y)) -> c_33(#positive^#(#natdiv(x, y)), #natdiv^#(x, y)) , #and^#(#true(), #true()) -> c_59() , #and^#(#true(), #false()) -> c_60() , #and^#(#false(), #true()) -> c_61() , #and^#(#false(), #false()) -> c_62() , #positive^#(#0()) -> c_68() , #positive^#(#s(x)) -> c_69() , #positive^#(#neg(x)) -> c_70() , #positive^#(#pos(x)) -> c_71() , #natdiv^#(#0(), #0()) -> c_63() , #natdiv^#(#0(), #s(y)) -> c_64() , #natdiv^#(#s(x), #0()) -> c_65() , #natdiv^#(#s(x), #s(y)) -> c_66(#natdiv'^#(#divsub(x, y), #s(y)), #divsub^#(x, y)) , #natdiv^#(#underflow(), y) -> c_67() , #negative^#(#0()) -> c_72() , #negative^#(#s(x)) -> c_73() , #negative^#(#neg(x)) -> c_74() , #negative^#(#pos(x)) -> c_75() , #natmult^#(#0(), y) -> c_76() , #natmult^#(#s(x), y) -> c_77(#natadd^#(y, #natmult(x, y)), #natmult^#(x, y)) , #add^#(#0(), y) -> c_46() , #add^#(#neg(#s(#0())), y) -> c_47(#pred^#(y)) , #add^#(#neg(#s(#s(x))), y) -> c_48(#pred^#(#add(#pos(#s(x)), y)), #add^#(#pos(#s(x)), y)) , #add^#(#pos(#s(#0())), y) -> c_49(#succ^#(y)) , #add^#(#pos(#s(#s(x))), y) -> c_50(#succ^#(#add(#pos(#s(x)), y)), #add^#(#pos(#s(x)), y)) , #pred^#(#0()) -> c_51() , #pred^#(#neg(#s(x))) -> c_52() , #pred^#(#pos(#s(#0()))) -> c_53() , #pred^#(#pos(#s(#s(x)))) -> c_54() , #succ^#(#0()) -> c_55() , #succ^#(#neg(#s(#0()))) -> c_56() , #succ^#(#neg(#s(#s(x)))) -> c_57() , #succ^#(#pos(#s(x))) -> c_58() , #natdiv'^#(#0(), y) -> c_82() , #natdiv'^#(#s(x), y) -> c_83(#natdiv^#(#s(x), y)) , #natdiv'^#(#underflow(), y) -> c_84() , #divsub^#(#0(), #0()) -> c_78() , #divsub^#(#0(), #s(y)) -> c_79() , #divsub^#(#s(x), #0()) -> c_80() , #divsub^#(#s(x), #s(y)) -> c_81(#divsub^#(x, y)) , #natadd^#(#0(), y) -> c_85() , #natadd^#(#s(x), y) -> c_86(#natadd^#(x, y)) , #natsub^#(#0(), #0()) -> c_87() , #natsub^#(#0(), #s(y)) -> c_88() , #natsub^#(#s(x), #0()) -> c_89() , #natsub^#(#s(x), #s(y)) -> c_90(#natsub^#(x, y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(::(x, xs)) -> c_2(eratos^#(filter(x, xs)), filter^#(x, xs)) , filter^#(p, ::(x, xs)) -> c_4(filter'^#(#equal(#mod(x, p), #0()), x, filter(p, xs)), #equal^#(#mod(x, p), #0()), #mod^#(x, p), filter^#(p, xs)) } Weak Trs: { #equal(x, y) -> #eq(x, y) , #eq(::(x_1, x_2), ::(y_1, y_2)) -> #and(#eq(x_1, y_1), #eq(x_2, y_2)) , #eq(::(x_1, x_2), nil()) -> #false() , #eq(nil(), ::(y_1, y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(y)) -> #false() , #eq(#0(), #neg(y)) -> #false() , #eq(#0(), #pos(y)) -> #false() , #eq(#s(x), #0()) -> #false() , #eq(#s(x), #s(y)) -> #eq(x, y) , #eq(#neg(x), #0()) -> #false() , #eq(#neg(x), #neg(y)) -> #eq(x, y) , #eq(#neg(x), #pos(y)) -> #false() , #eq(#pos(x), #0()) -> #false() , #eq(#pos(x), #neg(y)) -> #false() , #eq(#pos(x), #pos(y)) -> #eq(x, y) , eratos(::(x, xs)) -> ::(x, eratos(filter(x, xs))) , eratos(nil()) -> nil() , filter(p, ::(x, xs)) -> filter'(#equal(#mod(x, p), #0()), x, filter(p, xs)) , filter(p, nil()) -> nil() , #mod(x, y) -> #sub(x, #mult(y, #div(x, y))) , filter'(#true(), x, xs) -> xs , filter'(#false(), x, xs) -> ::(x, xs) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(y)) -> #0() , #div(#0(), #pos(y)) -> #0() , #div(#neg(x), #0()) -> #divByZero() , #div(#neg(x), #neg(y)) -> #positive(#natdiv(x, y)) , #div(#neg(x), #pos(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #0()) -> #divByZero() , #div(#pos(x), #neg(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #pos(y)) -> #positive(#natdiv(x, y)) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(y)) -> #0() , #mult(#0(), #pos(y)) -> #0() , #mult(#neg(x), #0()) -> #0() , #mult(#neg(x), #neg(y)) -> #pos(#natmult(x, y)) , #mult(#neg(x), #pos(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #0()) -> #0() , #mult(#pos(x), #neg(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #pos(y)) -> #pos(#natmult(x, y)) , #sub(x, #0()) -> x , #sub(x, #neg(y)) -> #add(x, #pos(y)) , #sub(x, #pos(y)) -> #add(x, #neg(y)) , #add(#0(), y) -> y , #add(#neg(#s(#0())), y) -> #pred(y) , #add(#neg(#s(#s(x))), y) -> #pred(#add(#pos(#s(x)), y)) , #add(#pos(#s(#0())), y) -> #succ(y) , #add(#pos(#s(#s(x))), y) -> #succ(#add(#pos(#s(x)), y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(x))) -> #neg(#s(#s(x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) , #succ(#pos(#s(x))) -> #pos(#s(#s(x))) , #and(#true(), #true()) -> #true() , #and(#true(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#false(), #false()) -> #false() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(y)) -> #0() , #natdiv(#s(x), #0()) -> #divByZero() , #natdiv(#s(x), #s(y)) -> #natdiv'(#divsub(x, y), #s(y)) , #natdiv(#underflow(), y) -> #0() , #positive(#0()) -> #0() , #positive(#s(x)) -> #pos(#s(x)) , #positive(#neg(x)) -> #neg(x) , #positive(#pos(x)) -> #pos(x) , #negative(#0()) -> #0() , #negative(#s(x)) -> #neg(#s(x)) , #negative(#neg(x)) -> #pos(x) , #negative(#pos(x)) -> #neg(x) , #natmult(#0(), y) -> #0() , #natmult(#s(x), y) -> #natadd(y, #natmult(x, y)) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(y)) -> #underflow() , #divsub(#s(x), #0()) -> #s(x) , #divsub(#s(x), #s(y)) -> #divsub(x, y) , #natdiv'(#0(), y) -> #s(#0()) , #natdiv'(#s(x), y) -> #s(#natdiv(#s(x), y)) , #natdiv'(#underflow(), y) -> #0() , #natadd(#0(), y) -> y , #natadd(#s(x), y) -> #s(#natadd(x, y)) , #natsub(#0(), #0()) -> #0() , #natsub(#0(), #s(y)) -> #0() , #natsub(#s(x), #0()) -> #s(x) , #natsub(#s(x), #s(y)) -> #natsub(x, y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { filter^#(p, ::(x, xs)) -> c_4(filter'^#(#equal(#mod(x, p), #0()), x, filter(p, xs)), #equal^#(#mod(x, p), #0()), #mod^#(x, p), filter^#(p, xs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(::(x, xs)) -> c_1(eratos^#(filter(x, xs)), filter^#(x, xs)) , filter^#(p, ::(x, xs)) -> c_2(filter^#(p, xs)) } Weak Trs: { #equal(x, y) -> #eq(x, y) , #eq(::(x_1, x_2), ::(y_1, y_2)) -> #and(#eq(x_1, y_1), #eq(x_2, y_2)) , #eq(::(x_1, x_2), nil()) -> #false() , #eq(nil(), ::(y_1, y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(y)) -> #false() , #eq(#0(), #neg(y)) -> #false() , #eq(#0(), #pos(y)) -> #false() , #eq(#s(x), #0()) -> #false() , #eq(#s(x), #s(y)) -> #eq(x, y) , #eq(#neg(x), #0()) -> #false() , #eq(#neg(x), #neg(y)) -> #eq(x, y) , #eq(#neg(x), #pos(y)) -> #false() , #eq(#pos(x), #0()) -> #false() , #eq(#pos(x), #neg(y)) -> #false() , #eq(#pos(x), #pos(y)) -> #eq(x, y) , eratos(::(x, xs)) -> ::(x, eratos(filter(x, xs))) , eratos(nil()) -> nil() , filter(p, ::(x, xs)) -> filter'(#equal(#mod(x, p), #0()), x, filter(p, xs)) , filter(p, nil()) -> nil() , #mod(x, y) -> #sub(x, #mult(y, #div(x, y))) , filter'(#true(), x, xs) -> xs , filter'(#false(), x, xs) -> ::(x, xs) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(y)) -> #0() , #div(#0(), #pos(y)) -> #0() , #div(#neg(x), #0()) -> #divByZero() , #div(#neg(x), #neg(y)) -> #positive(#natdiv(x, y)) , #div(#neg(x), #pos(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #0()) -> #divByZero() , #div(#pos(x), #neg(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #pos(y)) -> #positive(#natdiv(x, y)) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(y)) -> #0() , #mult(#0(), #pos(y)) -> #0() , #mult(#neg(x), #0()) -> #0() , #mult(#neg(x), #neg(y)) -> #pos(#natmult(x, y)) , #mult(#neg(x), #pos(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #0()) -> #0() , #mult(#pos(x), #neg(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #pos(y)) -> #pos(#natmult(x, y)) , #sub(x, #0()) -> x , #sub(x, #neg(y)) -> #add(x, #pos(y)) , #sub(x, #pos(y)) -> #add(x, #neg(y)) , #add(#0(), y) -> y , #add(#neg(#s(#0())), y) -> #pred(y) , #add(#neg(#s(#s(x))), y) -> #pred(#add(#pos(#s(x)), y)) , #add(#pos(#s(#0())), y) -> #succ(y) , #add(#pos(#s(#s(x))), y) -> #succ(#add(#pos(#s(x)), y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(x))) -> #neg(#s(#s(x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) , #succ(#pos(#s(x))) -> #pos(#s(#s(x))) , #and(#true(), #true()) -> #true() , #and(#true(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#false(), #false()) -> #false() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(y)) -> #0() , #natdiv(#s(x), #0()) -> #divByZero() , #natdiv(#s(x), #s(y)) -> #natdiv'(#divsub(x, y), #s(y)) , #natdiv(#underflow(), y) -> #0() , #positive(#0()) -> #0() , #positive(#s(x)) -> #pos(#s(x)) , #positive(#neg(x)) -> #neg(x) , #positive(#pos(x)) -> #pos(x) , #negative(#0()) -> #0() , #negative(#s(x)) -> #neg(#s(x)) , #negative(#neg(x)) -> #pos(x) , #negative(#pos(x)) -> #neg(x) , #natmult(#0(), y) -> #0() , #natmult(#s(x), y) -> #natadd(y, #natmult(x, y)) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(y)) -> #underflow() , #divsub(#s(x), #0()) -> #s(x) , #divsub(#s(x), #s(y)) -> #divsub(x, y) , #natdiv'(#0(), y) -> #s(#0()) , #natdiv'(#s(x), y) -> #s(#natdiv(#s(x), y)) , #natdiv'(#underflow(), y) -> #0() , #natadd(#0(), y) -> y , #natadd(#s(x), y) -> #s(#natadd(x, y)) , #natsub(#0(), #0()) -> #0() , #natsub(#0(), #s(y)) -> #0() , #natsub(#s(x), #0()) -> #s(x) , #natsub(#s(x), #s(y)) -> #natsub(x, y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We replace rewrite rules by usable rules: Weak Usable Rules: { #equal(x, y) -> #eq(x, y) , #eq(::(x_1, x_2), ::(y_1, y_2)) -> #and(#eq(x_1, y_1), #eq(x_2, y_2)) , #eq(::(x_1, x_2), nil()) -> #false() , #eq(nil(), ::(y_1, y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(y)) -> #false() , #eq(#0(), #neg(y)) -> #false() , #eq(#0(), #pos(y)) -> #false() , #eq(#s(x), #0()) -> #false() , #eq(#s(x), #s(y)) -> #eq(x, y) , #eq(#neg(x), #0()) -> #false() , #eq(#neg(x), #neg(y)) -> #eq(x, y) , #eq(#neg(x), #pos(y)) -> #false() , #eq(#pos(x), #0()) -> #false() , #eq(#pos(x), #neg(y)) -> #false() , #eq(#pos(x), #pos(y)) -> #eq(x, y) , filter(p, ::(x, xs)) -> filter'(#equal(#mod(x, p), #0()), x, filter(p, xs)) , filter(p, nil()) -> nil() , #mod(x, y) -> #sub(x, #mult(y, #div(x, y))) , filter'(#true(), x, xs) -> xs , filter'(#false(), x, xs) -> ::(x, xs) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(y)) -> #0() , #div(#0(), #pos(y)) -> #0() , #div(#neg(x), #0()) -> #divByZero() , #div(#neg(x), #neg(y)) -> #positive(#natdiv(x, y)) , #div(#neg(x), #pos(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #0()) -> #divByZero() , #div(#pos(x), #neg(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #pos(y)) -> #positive(#natdiv(x, y)) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(y)) -> #0() , #mult(#0(), #pos(y)) -> #0() , #mult(#neg(x), #0()) -> #0() , #mult(#neg(x), #neg(y)) -> #pos(#natmult(x, y)) , #mult(#neg(x), #pos(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #0()) -> #0() , #mult(#pos(x), #neg(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #pos(y)) -> #pos(#natmult(x, y)) , #sub(x, #0()) -> x , #sub(x, #neg(y)) -> #add(x, #pos(y)) , #sub(x, #pos(y)) -> #add(x, #neg(y)) , #add(#0(), y) -> y , #add(#neg(#s(#0())), y) -> #pred(y) , #add(#neg(#s(#s(x))), y) -> #pred(#add(#pos(#s(x)), y)) , #add(#pos(#s(#0())), y) -> #succ(y) , #add(#pos(#s(#s(x))), y) -> #succ(#add(#pos(#s(x)), y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(x))) -> #neg(#s(#s(x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) , #succ(#pos(#s(x))) -> #pos(#s(#s(x))) , #and(#true(), #true()) -> #true() , #and(#true(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#false(), #false()) -> #false() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(y)) -> #0() , #natdiv(#s(x), #0()) -> #divByZero() , #natdiv(#s(x), #s(y)) -> #natdiv'(#divsub(x, y), #s(y)) , #natdiv(#underflow(), y) -> #0() , #positive(#0()) -> #0() , #positive(#s(x)) -> #pos(#s(x)) , #positive(#neg(x)) -> #neg(x) , #positive(#pos(x)) -> #pos(x) , #negative(#0()) -> #0() , #negative(#s(x)) -> #neg(#s(x)) , #negative(#neg(x)) -> #pos(x) , #negative(#pos(x)) -> #neg(x) , #natmult(#0(), y) -> #0() , #natmult(#s(x), y) -> #natadd(y, #natmult(x, y)) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(y)) -> #underflow() , #divsub(#s(x), #0()) -> #s(x) , #divsub(#s(x), #s(y)) -> #divsub(x, y) , #natdiv'(#0(), y) -> #s(#0()) , #natdiv'(#s(x), y) -> #s(#natdiv(#s(x), y)) , #natdiv'(#underflow(), y) -> #0() , #natadd(#0(), y) -> y , #natadd(#s(x), y) -> #s(#natadd(x, y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(::(x, xs)) -> c_1(eratos^#(filter(x, xs)), filter^#(x, xs)) , filter^#(p, ::(x, xs)) -> c_2(filter^#(p, xs)) } Weak Trs: { #equal(x, y) -> #eq(x, y) , #eq(::(x_1, x_2), ::(y_1, y_2)) -> #and(#eq(x_1, y_1), #eq(x_2, y_2)) , #eq(::(x_1, x_2), nil()) -> #false() , #eq(nil(), ::(y_1, y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(y)) -> #false() , #eq(#0(), #neg(y)) -> #false() , #eq(#0(), #pos(y)) -> #false() , #eq(#s(x), #0()) -> #false() , #eq(#s(x), #s(y)) -> #eq(x, y) , #eq(#neg(x), #0()) -> #false() , #eq(#neg(x), #neg(y)) -> #eq(x, y) , #eq(#neg(x), #pos(y)) -> #false() , #eq(#pos(x), #0()) -> #false() , #eq(#pos(x), #neg(y)) -> #false() , #eq(#pos(x), #pos(y)) -> #eq(x, y) , filter(p, ::(x, xs)) -> filter'(#equal(#mod(x, p), #0()), x, filter(p, xs)) , filter(p, nil()) -> nil() , #mod(x, y) -> #sub(x, #mult(y, #div(x, y))) , filter'(#true(), x, xs) -> xs , filter'(#false(), x, xs) -> ::(x, xs) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(y)) -> #0() , #div(#0(), #pos(y)) -> #0() , #div(#neg(x), #0()) -> #divByZero() , #div(#neg(x), #neg(y)) -> #positive(#natdiv(x, y)) , #div(#neg(x), #pos(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #0()) -> #divByZero() , #div(#pos(x), #neg(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #pos(y)) -> #positive(#natdiv(x, y)) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(y)) -> #0() , #mult(#0(), #pos(y)) -> #0() , #mult(#neg(x), #0()) -> #0() , #mult(#neg(x), #neg(y)) -> #pos(#natmult(x, y)) , #mult(#neg(x), #pos(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #0()) -> #0() , #mult(#pos(x), #neg(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #pos(y)) -> #pos(#natmult(x, y)) , #sub(x, #0()) -> x , #sub(x, #neg(y)) -> #add(x, #pos(y)) , #sub(x, #pos(y)) -> #add(x, #neg(y)) , #add(#0(), y) -> y , #add(#neg(#s(#0())), y) -> #pred(y) , #add(#neg(#s(#s(x))), y) -> #pred(#add(#pos(#s(x)), y)) , #add(#pos(#s(#0())), y) -> #succ(y) , #add(#pos(#s(#s(x))), y) -> #succ(#add(#pos(#s(x)), y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(x))) -> #neg(#s(#s(x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) , #succ(#pos(#s(x))) -> #pos(#s(#s(x))) , #and(#true(), #true()) -> #true() , #and(#true(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#false(), #false()) -> #false() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(y)) -> #0() , #natdiv(#s(x), #0()) -> #divByZero() , #natdiv(#s(x), #s(y)) -> #natdiv'(#divsub(x, y), #s(y)) , #natdiv(#underflow(), y) -> #0() , #positive(#0()) -> #0() , #positive(#s(x)) -> #pos(#s(x)) , #positive(#neg(x)) -> #neg(x) , #positive(#pos(x)) -> #pos(x) , #negative(#0()) -> #0() , #negative(#s(x)) -> #neg(#s(x)) , #negative(#neg(x)) -> #pos(x) , #negative(#pos(x)) -> #neg(x) , #natmult(#0(), y) -> #0() , #natmult(#s(x), y) -> #natadd(y, #natmult(x, y)) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(y)) -> #underflow() , #divsub(#s(x), #0()) -> #s(x) , #divsub(#s(x), #s(y)) -> #divsub(x, y) , #natdiv'(#0(), y) -> #s(#0()) , #natdiv'(#s(x), y) -> #s(#natdiv(#s(x), y)) , #natdiv'(#underflow(), y) -> #0() , #natadd(#0(), y) -> y , #natadd(#s(x), y) -> #s(#natadd(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We decompose the input problem according to the dependency graph into the upper component { eratos^#(::(x, xs)) -> c_1(eratos^#(filter(x, xs)), filter^#(x, xs)) } and lower component { filter^#(p, ::(x, xs)) -> c_2(filter^#(p, xs)) } Further, following extension rules are added to the lower component. { eratos^#(::(x, xs)) -> eratos^#(filter(x, xs)) , eratos^#(::(x, xs)) -> filter^#(x, xs) } TcT solves the upper component with certificate YES(O(1),O(n^1)). Sub-proof: ---------- We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { eratos^#(::(x, xs)) -> c_1(eratos^#(filter(x, xs)), filter^#(x, xs)) } Weak Trs: { #equal(x, y) -> #eq(x, y) , #eq(::(x_1, x_2), ::(y_1, y_2)) -> #and(#eq(x_1, y_1), #eq(x_2, y_2)) , #eq(::(x_1, x_2), nil()) -> #false() , #eq(nil(), ::(y_1, y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(y)) -> #false() , #eq(#0(), #neg(y)) -> #false() , #eq(#0(), #pos(y)) -> #false() , #eq(#s(x), #0()) -> #false() , #eq(#s(x), #s(y)) -> #eq(x, y) , #eq(#neg(x), #0()) -> #false() , #eq(#neg(x), #neg(y)) -> #eq(x, y) , #eq(#neg(x), #pos(y)) -> #false() , #eq(#pos(x), #0()) -> #false() , #eq(#pos(x), #neg(y)) -> #false() , #eq(#pos(x), #pos(y)) -> #eq(x, y) , filter(p, ::(x, xs)) -> filter'(#equal(#mod(x, p), #0()), x, filter(p, xs)) , filter(p, nil()) -> nil() , #mod(x, y) -> #sub(x, #mult(y, #div(x, y))) , filter'(#true(), x, xs) -> xs , filter'(#false(), x, xs) -> ::(x, xs) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(y)) -> #0() , #div(#0(), #pos(y)) -> #0() , #div(#neg(x), #0()) -> #divByZero() , #div(#neg(x), #neg(y)) -> #positive(#natdiv(x, y)) , #div(#neg(x), #pos(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #0()) -> #divByZero() , #div(#pos(x), #neg(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #pos(y)) -> #positive(#natdiv(x, y)) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(y)) -> #0() , #mult(#0(), #pos(y)) -> #0() , #mult(#neg(x), #0()) -> #0() , #mult(#neg(x), #neg(y)) -> #pos(#natmult(x, y)) , #mult(#neg(x), #pos(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #0()) -> #0() , #mult(#pos(x), #neg(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #pos(y)) -> #pos(#natmult(x, y)) , #sub(x, #0()) -> x , #sub(x, #neg(y)) -> #add(x, #pos(y)) , #sub(x, #pos(y)) -> #add(x, #neg(y)) , #add(#0(), y) -> y , #add(#neg(#s(#0())), y) -> #pred(y) , #add(#neg(#s(#s(x))), y) -> #pred(#add(#pos(#s(x)), y)) , #add(#pos(#s(#0())), y) -> #succ(y) , #add(#pos(#s(#s(x))), y) -> #succ(#add(#pos(#s(x)), y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(x))) -> #neg(#s(#s(x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) , #succ(#pos(#s(x))) -> #pos(#s(#s(x))) , #and(#true(), #true()) -> #true() , #and(#true(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#false(), #false()) -> #false() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(y)) -> #0() , #natdiv(#s(x), #0()) -> #divByZero() , #natdiv(#s(x), #s(y)) -> #natdiv'(#divsub(x, y), #s(y)) , #natdiv(#underflow(), y) -> #0() , #positive(#0()) -> #0() , #positive(#s(x)) -> #pos(#s(x)) , #positive(#neg(x)) -> #neg(x) , #positive(#pos(x)) -> #pos(x) , #negative(#0()) -> #0() , #negative(#s(x)) -> #neg(#s(x)) , #negative(#neg(x)) -> #pos(x) , #negative(#pos(x)) -> #neg(x) , #natmult(#0(), y) -> #0() , #natmult(#s(x), y) -> #natadd(y, #natmult(x, y)) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(y)) -> #underflow() , #divsub(#s(x), #0()) -> #s(x) , #divsub(#s(x), #s(y)) -> #divsub(x, y) , #natdiv'(#0(), y) -> #s(#0()) , #natdiv'(#s(x), y) -> #s(#natdiv(#s(x), y)) , #natdiv'(#underflow(), y) -> #0() , #natadd(#0(), y) -> y , #natadd(#s(x), y) -> #s(#natadd(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { eratos^#(::(x, xs)) -> c_1(eratos^#(filter(x, xs)), filter^#(x, xs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { eratos^#(::(x, xs)) -> c_1(eratos^#(filter(x, xs))) } Weak Trs: { #equal(x, y) -> #eq(x, y) , #eq(::(x_1, x_2), ::(y_1, y_2)) -> #and(#eq(x_1, y_1), #eq(x_2, y_2)) , #eq(::(x_1, x_2), nil()) -> #false() , #eq(nil(), ::(y_1, y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(y)) -> #false() , #eq(#0(), #neg(y)) -> #false() , #eq(#0(), #pos(y)) -> #false() , #eq(#s(x), #0()) -> #false() , #eq(#s(x), #s(y)) -> #eq(x, y) , #eq(#neg(x), #0()) -> #false() , #eq(#neg(x), #neg(y)) -> #eq(x, y) , #eq(#neg(x), #pos(y)) -> #false() , #eq(#pos(x), #0()) -> #false() , #eq(#pos(x), #neg(y)) -> #false() , #eq(#pos(x), #pos(y)) -> #eq(x, y) , filter(p, ::(x, xs)) -> filter'(#equal(#mod(x, p), #0()), x, filter(p, xs)) , filter(p, nil()) -> nil() , #mod(x, y) -> #sub(x, #mult(y, #div(x, y))) , filter'(#true(), x, xs) -> xs , filter'(#false(), x, xs) -> ::(x, xs) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(y)) -> #0() , #div(#0(), #pos(y)) -> #0() , #div(#neg(x), #0()) -> #divByZero() , #div(#neg(x), #neg(y)) -> #positive(#natdiv(x, y)) , #div(#neg(x), #pos(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #0()) -> #divByZero() , #div(#pos(x), #neg(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #pos(y)) -> #positive(#natdiv(x, y)) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(y)) -> #0() , #mult(#0(), #pos(y)) -> #0() , #mult(#neg(x), #0()) -> #0() , #mult(#neg(x), #neg(y)) -> #pos(#natmult(x, y)) , #mult(#neg(x), #pos(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #0()) -> #0() , #mult(#pos(x), #neg(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #pos(y)) -> #pos(#natmult(x, y)) , #sub(x, #0()) -> x , #sub(x, #neg(y)) -> #add(x, #pos(y)) , #sub(x, #pos(y)) -> #add(x, #neg(y)) , #add(#0(), y) -> y , #add(#neg(#s(#0())), y) -> #pred(y) , #add(#neg(#s(#s(x))), y) -> #pred(#add(#pos(#s(x)), y)) , #add(#pos(#s(#0())), y) -> #succ(y) , #add(#pos(#s(#s(x))), y) -> #succ(#add(#pos(#s(x)), y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(x))) -> #neg(#s(#s(x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) , #succ(#pos(#s(x))) -> #pos(#s(#s(x))) , #and(#true(), #true()) -> #true() , #and(#true(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#false(), #false()) -> #false() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(y)) -> #0() , #natdiv(#s(x), #0()) -> #divByZero() , #natdiv(#s(x), #s(y)) -> #natdiv'(#divsub(x, y), #s(y)) , #natdiv(#underflow(), y) -> #0() , #positive(#0()) -> #0() , #positive(#s(x)) -> #pos(#s(x)) , #positive(#neg(x)) -> #neg(x) , #positive(#pos(x)) -> #pos(x) , #negative(#0()) -> #0() , #negative(#s(x)) -> #neg(#s(x)) , #negative(#neg(x)) -> #pos(x) , #negative(#pos(x)) -> #neg(x) , #natmult(#0(), y) -> #0() , #natmult(#s(x), y) -> #natadd(y, #natmult(x, y)) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(y)) -> #underflow() , #divsub(#s(x), #0()) -> #s(x) , #divsub(#s(x), #s(y)) -> #divsub(x, y) , #natdiv'(#0(), y) -> #s(#0()) , #natdiv'(#s(x), y) -> #s(#natdiv(#s(x), y)) , #natdiv'(#underflow(), y) -> #0() , #natadd(#0(), y) -> y , #natadd(#s(x), y) -> #s(#natadd(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: eratos^#(::(x, xs)) -> c_1(eratos^#(filter(x, xs))) } Trs: { #eq(::(x_1, x_2), ::(y_1, y_2)) -> #and(#eq(x_1, y_1), #eq(x_2, y_2)) , #eq(::(x_1, x_2), nil()) -> #false() , #eq(nil(), ::(y_1, y_2)) -> #false() , #eq(#0(), #s(y)) -> #false() , #eq(#0(), #pos(y)) -> #false() , #eq(#s(x), #0()) -> #false() , #eq(#s(x), #s(y)) -> #eq(x, y) , #eq(#neg(x), #pos(y)) -> #false() , #eq(#pos(x), #0()) -> #false() , #eq(#pos(x), #neg(y)) -> #false() , #eq(#pos(x), #pos(y)) -> #eq(x, y) , filter'(#true(), x, xs) -> xs , #div(#0(), #neg(y)) -> #0() , #div(#0(), #pos(y)) -> #0() , #div(#neg(x), #pos(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #0()) -> #divByZero() , #div(#pos(x), #neg(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #pos(y)) -> #positive(#natdiv(x, y)) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(y)) -> #0() , #mult(#0(), #pos(y)) -> #0() , #mult(#neg(x), #0()) -> #0() , #mult(#neg(x), #pos(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #0()) -> #0() , #mult(#pos(x), #neg(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #pos(y)) -> #pos(#natmult(x, y)) , #sub(x, #0()) -> x , #add(#neg(#s(#s(x))), y) -> #pred(#add(#pos(#s(x)), y)) , #add(#pos(#s(#0())), y) -> #succ(y) , #add(#pos(#s(#s(x))), y) -> #succ(#add(#pos(#s(x)), y)) , #pred(#pos(#s(#0()))) -> #0() , #succ(#neg(#s(#0()))) -> #0() , #and(#true(), #true()) -> #true() , #and(#true(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#false(), #false()) -> #false() , #natdiv(#0(), #s(y)) -> #0() , #natdiv(#underflow(), y) -> #0() , #positive(#0()) -> #0() , #positive(#neg(x)) -> #neg(x) , #positive(#pos(x)) -> #pos(x) , #negative(#0()) -> #0() , #negative(#s(x)) -> #neg(#s(x)) , #negative(#pos(x)) -> #neg(x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(y)) -> #underflow() , #divsub(#s(x), #0()) -> #s(x) , #divsub(#s(x), #s(y)) -> #divsub(x, y) , #natdiv'(#underflow(), y) -> #0() } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#equal](x1, x2) = [1] x1 + [1] x2 + [1] [#eq](x1, x2) = [1] x1 + [1] x2 + [1] [::](x1, x2) = [1] x1 + [1] x2 + [1] [filter](x1, x2) = [1] x2 + [0] [nil] = [0] [#mod](x1, x2) = [1] x1 + [1] x2 + [1] [#0] = [0] [filter'](x1, x2, x3) = [1] x2 + [1] x3 + [1] [#true] = [1] [#false] = [1] [#div](x1, x2) = [1] x1 + [1] x2 + [1] [#mult](x1, x2) = [1] x1 + [1] x2 + [1] [#sub](x1, x2) = [1] x1 + [1] [#add](x1, x2) = [1] x1 + [1] x2 + [0] [#s](x1) = [1] x1 + [1] [#neg](x1) = [1] x1 + [0] [#pred](x1) = [1] [#pos](x1) = [1] x1 + [1] [#succ](x1) = [1] [#and](x1, x2) = [1] x2 + [1] [#divByZero] = [1] [#natdiv](x1, x2) = [1] x1 + [1] x2 + [0] [#positive](x1) = [1] x1 + [1] [#negative](x1) = [1] x1 + [1] [#natmult](x1, x2) = [1] x1 + [1] x2 + [0] [#divsub](x1, x2) = [1] x1 + [1] x2 + [1] [#natdiv'](x1, x2) = [1] x1 + [1] x2 + [0] [#underflow] = [1] [#natadd](x1, x2) = [1] x1 + [1] x2 + [0] [eratos^#](x1) = [1] x1 + [1] [filter^#](x1, x2) = [1] x1 + [1] x2 + [0] [c_1](x1, x2) = [1] x1 + [1] x2 + [0] [c] = [0] [c_1](x1) = [1] x1 + [0] This order satisfies following ordering constraints [#eq(::(x_1, x_2), ::(y_1, y_2))] = [1] x_1 + [1] x_2 + [1] y_1 + [1] y_2 + [3] > [1] x_2 + [1] y_2 + [2] = [#and(#eq(x_1, y_1), #eq(x_2, y_2))] [#eq(::(x_1, x_2), nil())] = [1] x_1 + [1] x_2 + [2] > [1] = [#false()] [#eq(nil(), ::(y_1, y_2))] = [1] y_1 + [1] y_2 + [2] > [1] = [#false()] [#eq(nil(), nil())] = [1] >= [1] = [#true()] [#eq(#0(), #0())] = [1] >= [1] = [#true()] [#eq(#0(), #s(y))] = [1] y + [2] > [1] = [#false()] [#eq(#0(), #neg(y))] = [1] y + [1] >= [1] = [#false()] [#eq(#0(), #pos(y))] = [1] y + [2] > [1] = [#false()] [#eq(#s(x), #0())] = [1] x + [2] > [1] = [#false()] [#eq(#s(x), #s(y))] = [1] x + [1] y + [3] > [1] x + [1] y + [1] = [#eq(x, y)] [#eq(#neg(x), #0())] = [1] x + [1] >= [1] = [#false()] [#eq(#neg(x), #neg(y))] = [1] x + [1] y + [1] >= [1] x + [1] y + [1] = [#eq(x, y)] [#eq(#neg(x), #pos(y))] = [1] x + [1] y + [2] > [1] = [#false()] [#eq(#pos(x), #0())] = [1] x + [2] > [1] = [#false()] [#eq(#pos(x), #neg(y))] = [1] x + [1] y + [2] > [1] = [#false()] [#eq(#pos(x), #pos(y))] = [1] x + [1] y + [3] > [1] x + [1] y + [1] = [#eq(x, y)] [filter(p, ::(x, xs))] = [1] x + [1] xs + [1] >= [1] x + [1] xs + [1] = [filter'(#equal(#mod(x, p), #0()), x, filter(p, xs))] [filter(p, nil())] = [0] >= [0] = [nil()] [filter'(#true(), x, xs)] = [1] x + [1] xs + [1] > [1] xs + [0] = [xs] [filter'(#false(), x, xs)] = [1] x + [1] xs + [1] >= [1] x + [1] xs + [1] = [::(x, xs)] [#and(#true(), #true())] = [2] > [1] = [#true()] [#and(#true(), #false())] = [2] > [1] = [#false()] [#and(#false(), #true())] = [2] > [1] = [#false()] [#and(#false(), #false())] = [2] > [1] = [#false()] [#positive(#0())] = [1] > [0] = [#0()] [#positive(#s(x))] = [1] x + [2] >= [1] x + [2] = [#pos(#s(x))] [#positive(#neg(x))] = [1] x + [1] > [1] x + [0] = [#neg(x)] [#positive(#pos(x))] = [1] x + [2] > [1] x + [1] = [#pos(x)] [#negative(#0())] = [1] > [0] = [#0()] [#negative(#s(x))] = [1] x + [2] > [1] x + [1] = [#neg(#s(x))] [#negative(#neg(x))] = [1] x + [1] >= [1] x + [1] = [#pos(x)] [#negative(#pos(x))] = [1] x + [2] > [1] x + [0] = [#neg(x)] [#divsub(#0(), #0())] = [1] > [0] = [#0()] [#divsub(#0(), #s(y))] = [1] y + [2] > [1] = [#underflow()] [#divsub(#s(x), #0())] = [1] x + [2] > [1] x + [1] = [#s(x)] [#divsub(#s(x), #s(y))] = [1] x + [1] y + [3] > [1] x + [1] y + [1] = [#divsub(x, y)] [eratos^#(::(x, xs))] = [1] x + [1] xs + [2] > [1] xs + [1] = [c_1(eratos^#(filter(x, xs)))] The strictly oriented rules are moved into the corresponding weak component(s). We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { eratos^#(::(x, xs)) -> c_1(eratos^#(filter(x, xs))) } Weak Trs: { #equal(x, y) -> #eq(x, y) , #eq(::(x_1, x_2), ::(y_1, y_2)) -> #and(#eq(x_1, y_1), #eq(x_2, y_2)) , #eq(::(x_1, x_2), nil()) -> #false() , #eq(nil(), ::(y_1, y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(y)) -> #false() , #eq(#0(), #neg(y)) -> #false() , #eq(#0(), #pos(y)) -> #false() , #eq(#s(x), #0()) -> #false() , #eq(#s(x), #s(y)) -> #eq(x, y) , #eq(#neg(x), #0()) -> #false() , #eq(#neg(x), #neg(y)) -> #eq(x, y) , #eq(#neg(x), #pos(y)) -> #false() , #eq(#pos(x), #0()) -> #false() , #eq(#pos(x), #neg(y)) -> #false() , #eq(#pos(x), #pos(y)) -> #eq(x, y) , filter(p, ::(x, xs)) -> filter'(#equal(#mod(x, p), #0()), x, filter(p, xs)) , filter(p, nil()) -> nil() , #mod(x, y) -> #sub(x, #mult(y, #div(x, y))) , filter'(#true(), x, xs) -> xs , filter'(#false(), x, xs) -> ::(x, xs) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(y)) -> #0() , #div(#0(), #pos(y)) -> #0() , #div(#neg(x), #0()) -> #divByZero() , #div(#neg(x), #neg(y)) -> #positive(#natdiv(x, y)) , #div(#neg(x), #pos(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #0()) -> #divByZero() , #div(#pos(x), #neg(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #pos(y)) -> #positive(#natdiv(x, y)) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(y)) -> #0() , #mult(#0(), #pos(y)) -> #0() , #mult(#neg(x), #0()) -> #0() , #mult(#neg(x), #neg(y)) -> #pos(#natmult(x, y)) , #mult(#neg(x), #pos(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #0()) -> #0() , #mult(#pos(x), #neg(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #pos(y)) -> #pos(#natmult(x, y)) , #sub(x, #0()) -> x , #sub(x, #neg(y)) -> #add(x, #pos(y)) , #sub(x, #pos(y)) -> #add(x, #neg(y)) , #add(#0(), y) -> y , #add(#neg(#s(#0())), y) -> #pred(y) , #add(#neg(#s(#s(x))), y) -> #pred(#add(#pos(#s(x)), y)) , #add(#pos(#s(#0())), y) -> #succ(y) , #add(#pos(#s(#s(x))), y) -> #succ(#add(#pos(#s(x)), y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(x))) -> #neg(#s(#s(x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) , #succ(#pos(#s(x))) -> #pos(#s(#s(x))) , #and(#true(), #true()) -> #true() , #and(#true(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#false(), #false()) -> #false() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(y)) -> #0() , #natdiv(#s(x), #0()) -> #divByZero() , #natdiv(#s(x), #s(y)) -> #natdiv'(#divsub(x, y), #s(y)) , #natdiv(#underflow(), y) -> #0() , #positive(#0()) -> #0() , #positive(#s(x)) -> #pos(#s(x)) , #positive(#neg(x)) -> #neg(x) , #positive(#pos(x)) -> #pos(x) , #negative(#0()) -> #0() , #negative(#s(x)) -> #neg(#s(x)) , #negative(#neg(x)) -> #pos(x) , #negative(#pos(x)) -> #neg(x) , #natmult(#0(), y) -> #0() , #natmult(#s(x), y) -> #natadd(y, #natmult(x, y)) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(y)) -> #underflow() , #divsub(#s(x), #0()) -> #s(x) , #divsub(#s(x), #s(y)) -> #divsub(x, y) , #natdiv'(#0(), y) -> #s(#0()) , #natdiv'(#s(x), y) -> #s(#natdiv(#s(x), y)) , #natdiv'(#underflow(), y) -> #0() , #natadd(#0(), y) -> y , #natadd(#s(x), y) -> #s(#natadd(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { eratos^#(::(x, xs)) -> c_1(eratos^#(filter(x, xs))) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { #equal(x, y) -> #eq(x, y) , #eq(::(x_1, x_2), ::(y_1, y_2)) -> #and(#eq(x_1, y_1), #eq(x_2, y_2)) , #eq(::(x_1, x_2), nil()) -> #false() , #eq(nil(), ::(y_1, y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(y)) -> #false() , #eq(#0(), #neg(y)) -> #false() , #eq(#0(), #pos(y)) -> #false() , #eq(#s(x), #0()) -> #false() , #eq(#s(x), #s(y)) -> #eq(x, y) , #eq(#neg(x), #0()) -> #false() , #eq(#neg(x), #neg(y)) -> #eq(x, y) , #eq(#neg(x), #pos(y)) -> #false() , #eq(#pos(x), #0()) -> #false() , #eq(#pos(x), #neg(y)) -> #false() , #eq(#pos(x), #pos(y)) -> #eq(x, y) , filter(p, ::(x, xs)) -> filter'(#equal(#mod(x, p), #0()), x, filter(p, xs)) , filter(p, nil()) -> nil() , #mod(x, y) -> #sub(x, #mult(y, #div(x, y))) , filter'(#true(), x, xs) -> xs , filter'(#false(), x, xs) -> ::(x, xs) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(y)) -> #0() , #div(#0(), #pos(y)) -> #0() , #div(#neg(x), #0()) -> #divByZero() , #div(#neg(x), #neg(y)) -> #positive(#natdiv(x, y)) , #div(#neg(x), #pos(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #0()) -> #divByZero() , #div(#pos(x), #neg(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #pos(y)) -> #positive(#natdiv(x, y)) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(y)) -> #0() , #mult(#0(), #pos(y)) -> #0() , #mult(#neg(x), #0()) -> #0() , #mult(#neg(x), #neg(y)) -> #pos(#natmult(x, y)) , #mult(#neg(x), #pos(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #0()) -> #0() , #mult(#pos(x), #neg(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #pos(y)) -> #pos(#natmult(x, y)) , #sub(x, #0()) -> x , #sub(x, #neg(y)) -> #add(x, #pos(y)) , #sub(x, #pos(y)) -> #add(x, #neg(y)) , #add(#0(), y) -> y , #add(#neg(#s(#0())), y) -> #pred(y) , #add(#neg(#s(#s(x))), y) -> #pred(#add(#pos(#s(x)), y)) , #add(#pos(#s(#0())), y) -> #succ(y) , #add(#pos(#s(#s(x))), y) -> #succ(#add(#pos(#s(x)), y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(x))) -> #neg(#s(#s(x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) , #succ(#pos(#s(x))) -> #pos(#s(#s(x))) , #and(#true(), #true()) -> #true() , #and(#true(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#false(), #false()) -> #false() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(y)) -> #0() , #natdiv(#s(x), #0()) -> #divByZero() , #natdiv(#s(x), #s(y)) -> #natdiv'(#divsub(x, y), #s(y)) , #natdiv(#underflow(), y) -> #0() , #positive(#0()) -> #0() , #positive(#s(x)) -> #pos(#s(x)) , #positive(#neg(x)) -> #neg(x) , #positive(#pos(x)) -> #pos(x) , #negative(#0()) -> #0() , #negative(#s(x)) -> #neg(#s(x)) , #negative(#neg(x)) -> #pos(x) , #negative(#pos(x)) -> #neg(x) , #natmult(#0(), y) -> #0() , #natmult(#s(x), y) -> #natadd(y, #natmult(x, y)) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(y)) -> #underflow() , #divsub(#s(x), #0()) -> #s(x) , #divsub(#s(x), #s(y)) -> #divsub(x, y) , #natdiv'(#0(), y) -> #s(#0()) , #natdiv'(#s(x), y) -> #s(#natdiv(#s(x), y)) , #natdiv'(#underflow(), y) -> #0() , #natadd(#0(), y) -> y , #natadd(#s(x), y) -> #s(#natadd(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { filter^#(p, ::(x, xs)) -> c_2(filter^#(p, xs)) } Weak DPs: { eratos^#(::(x, xs)) -> eratos^#(filter(x, xs)) , eratos^#(::(x, xs)) -> filter^#(x, xs) } Weak Trs: { #equal(x, y) -> #eq(x, y) , #eq(::(x_1, x_2), ::(y_1, y_2)) -> #and(#eq(x_1, y_1), #eq(x_2, y_2)) , #eq(::(x_1, x_2), nil()) -> #false() , #eq(nil(), ::(y_1, y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(y)) -> #false() , #eq(#0(), #neg(y)) -> #false() , #eq(#0(), #pos(y)) -> #false() , #eq(#s(x), #0()) -> #false() , #eq(#s(x), #s(y)) -> #eq(x, y) , #eq(#neg(x), #0()) -> #false() , #eq(#neg(x), #neg(y)) -> #eq(x, y) , #eq(#neg(x), #pos(y)) -> #false() , #eq(#pos(x), #0()) -> #false() , #eq(#pos(x), #neg(y)) -> #false() , #eq(#pos(x), #pos(y)) -> #eq(x, y) , filter(p, ::(x, xs)) -> filter'(#equal(#mod(x, p), #0()), x, filter(p, xs)) , filter(p, nil()) -> nil() , #mod(x, y) -> #sub(x, #mult(y, #div(x, y))) , filter'(#true(), x, xs) -> xs , filter'(#false(), x, xs) -> ::(x, xs) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(y)) -> #0() , #div(#0(), #pos(y)) -> #0() , #div(#neg(x), #0()) -> #divByZero() , #div(#neg(x), #neg(y)) -> #positive(#natdiv(x, y)) , #div(#neg(x), #pos(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #0()) -> #divByZero() , #div(#pos(x), #neg(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #pos(y)) -> #positive(#natdiv(x, y)) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(y)) -> #0() , #mult(#0(), #pos(y)) -> #0() , #mult(#neg(x), #0()) -> #0() , #mult(#neg(x), #neg(y)) -> #pos(#natmult(x, y)) , #mult(#neg(x), #pos(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #0()) -> #0() , #mult(#pos(x), #neg(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #pos(y)) -> #pos(#natmult(x, y)) , #sub(x, #0()) -> x , #sub(x, #neg(y)) -> #add(x, #pos(y)) , #sub(x, #pos(y)) -> #add(x, #neg(y)) , #add(#0(), y) -> y , #add(#neg(#s(#0())), y) -> #pred(y) , #add(#neg(#s(#s(x))), y) -> #pred(#add(#pos(#s(x)), y)) , #add(#pos(#s(#0())), y) -> #succ(y) , #add(#pos(#s(#s(x))), y) -> #succ(#add(#pos(#s(x)), y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(x))) -> #neg(#s(#s(x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) , #succ(#pos(#s(x))) -> #pos(#s(#s(x))) , #and(#true(), #true()) -> #true() , #and(#true(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#false(), #false()) -> #false() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(y)) -> #0() , #natdiv(#s(x), #0()) -> #divByZero() , #natdiv(#s(x), #s(y)) -> #natdiv'(#divsub(x, y), #s(y)) , #natdiv(#underflow(), y) -> #0() , #positive(#0()) -> #0() , #positive(#s(x)) -> #pos(#s(x)) , #positive(#neg(x)) -> #neg(x) , #positive(#pos(x)) -> #pos(x) , #negative(#0()) -> #0() , #negative(#s(x)) -> #neg(#s(x)) , #negative(#neg(x)) -> #pos(x) , #negative(#pos(x)) -> #neg(x) , #natmult(#0(), y) -> #0() , #natmult(#s(x), y) -> #natadd(y, #natmult(x, y)) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(y)) -> #underflow() , #divsub(#s(x), #0()) -> #s(x) , #divsub(#s(x), #s(y)) -> #divsub(x, y) , #natdiv'(#0(), y) -> #s(#0()) , #natdiv'(#s(x), y) -> #s(#natdiv(#s(x), y)) , #natdiv'(#underflow(), y) -> #0() , #natadd(#0(), y) -> y , #natadd(#s(x), y) -> #s(#natadd(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 1: filter^#(p, ::(x, xs)) -> c_2(filter^#(p, xs)) , 3: eratos^#(::(x, xs)) -> filter^#(x, xs) } Trs: { filter(p, nil()) -> nil() , filter'(#true(), x, xs) -> xs , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(y)) -> #0() , #div(#0(), #pos(y)) -> #0() , #div(#neg(x), #0()) -> #divByZero() , #div(#pos(x), #0()) -> #divByZero() , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(y)) -> #0() , #mult(#0(), #pos(y)) -> #0() , #mult(#neg(x), #0()) -> #0() , #mult(#pos(x), #0()) -> #0() , #sub(x, #0()) -> x , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) , #positive(#0()) -> #0() , #positive(#neg(x)) -> #neg(x) , #positive(#pos(x)) -> #pos(x) , #negative(#0()) -> #0() , #negative(#neg(x)) -> #pos(x) , #negative(#pos(x)) -> #neg(x) , #divsub(#s(x), #s(y)) -> #divsub(x, y) , #natdiv'(#s(x), y) -> #s(#natdiv(#s(x), y)) , #natdiv'(#underflow(), y) -> #0() , #natadd(#0(), y) -> y } Sub-proof: ---------- The following argument positions are usable: Uargs(c_2) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#equal](x1, x2) = [0] [#eq](x1, x2) = [0] [::](x1, x2) = [1] x1 + [1] x2 + [1] [filter](x1, x2) = [1] x1 + [1] x2 + [1] [nil] = [1] [#mod](x1, x2) = [1] x1 + [1] x2 + [1] [#0] = [1] [filter'](x1, x2, x3) = [1] x1 + [1] x2 + [1] x3 + [1] [#true] = [0] [#false] = [0] [#div](x1, x2) = [1] x1 + [1] [#mult](x1, x2) = [1] x2 + [1] [#sub](x1, x2) = [1] x1 + [1] [#add](x1, x2) = [1] [#s](x1) = [1] x1 + [1] [#neg](x1) = [1] x1 + [1] [#pred](x1) = [1] x1 + [0] [#pos](x1) = [1] x1 + [1] [#succ](x1) = [1] x1 + [0] [#and](x1, x2) = [1] x1 + [1] x2 + [0] [#divByZero] = [1] [#natdiv](x1, x2) = [1] x2 + [0] [#positive](x1) = [1] x1 + [1] [#negative](x1) = [1] x1 + [1] [#natmult](x1, x2) = [1] x1 + [1] x2 + [0] [#divsub](x1, x2) = [1] x2 + [0] [#natdiv'](x1, x2) = [1] x1 + [1] x2 + [1] [#underflow] = [1] [#natadd](x1, x2) = [1] x1 + [1] x2 + [0] [eratos^#](x1) = [1] x1 + [1] [filter^#](x1, x2) = [1] x1 + [1] x2 + [0] [c_2](x1) = [1] x1 + [0] This order satisfies following ordering constraints [#equal(x, y)] = [0] >= [0] = [#eq(x, y)] [#eq(::(x_1, x_2), ::(y_1, y_2))] = [0] >= [0] = [#and(#eq(x_1, y_1), #eq(x_2, y_2))] [#eq(::(x_1, x_2), nil())] = [0] >= [0] = [#false()] [#eq(nil(), ::(y_1, y_2))] = [0] >= [0] = [#false()] [#eq(nil(), nil())] = [0] >= [0] = [#true()] [#eq(#0(), #0())] = [0] >= [0] = [#true()] [#eq(#0(), #s(y))] = [0] >= [0] = [#false()] [#eq(#0(), #neg(y))] = [0] >= [0] = [#false()] [#eq(#0(), #pos(y))] = [0] >= [0] = [#false()] [#eq(#s(x), #0())] = [0] >= [0] = [#false()] [#eq(#s(x), #s(y))] = [0] >= [0] = [#eq(x, y)] [#eq(#neg(x), #0())] = [0] >= [0] = [#false()] [#eq(#neg(x), #neg(y))] = [0] >= [0] = [#eq(x, y)] [#eq(#neg(x), #pos(y))] = [0] >= [0] = [#false()] [#eq(#pos(x), #0())] = [0] >= [0] = [#false()] [#eq(#pos(x), #neg(y))] = [0] >= [0] = [#false()] [#eq(#pos(x), #pos(y))] = [0] >= [0] = [#eq(x, y)] [filter(p, ::(x, xs))] = [1] p + [1] x + [1] xs + [2] >= [1] p + [1] x + [1] xs + [2] = [filter'(#equal(#mod(x, p), #0()), x, filter(p, xs))] [filter(p, nil())] = [1] p + [2] > [1] = [nil()] [filter'(#true(), x, xs)] = [1] x + [1] xs + [1] > [1] xs + [0] = [xs] [filter'(#false(), x, xs)] = [1] x + [1] xs + [1] >= [1] x + [1] xs + [1] = [::(x, xs)] [#and(#true(), #true())] = [0] >= [0] = [#true()] [#and(#true(), #false())] = [0] >= [0] = [#false()] [#and(#false(), #true())] = [0] >= [0] = [#false()] [#and(#false(), #false())] = [0] >= [0] = [#false()] [#negative(#0())] = [2] > [1] = [#0()] [#negative(#s(x))] = [1] x + [2] >= [1] x + [2] = [#neg(#s(x))] [#negative(#neg(x))] = [1] x + [2] > [1] x + [1] = [#pos(x)] [#negative(#pos(x))] = [1] x + [2] > [1] x + [1] = [#neg(x)] [eratos^#(::(x, xs))] = [1] x + [1] xs + [2] >= [1] x + [1] xs + [2] = [eratos^#(filter(x, xs))] [eratos^#(::(x, xs))] = [1] x + [1] xs + [2] > [1] x + [1] xs + [0] = [filter^#(x, xs)] [filter^#(p, ::(x, xs))] = [1] p + [1] x + [1] xs + [1] > [1] p + [1] xs + [0] = [c_2(filter^#(p, xs))] The strictly oriented rules are moved into the corresponding weak component(s). We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak DPs: { eratos^#(::(x, xs)) -> eratos^#(filter(x, xs)) , eratos^#(::(x, xs)) -> filter^#(x, xs) , filter^#(p, ::(x, xs)) -> c_2(filter^#(p, xs)) } Weak Trs: { #equal(x, y) -> #eq(x, y) , #eq(::(x_1, x_2), ::(y_1, y_2)) -> #and(#eq(x_1, y_1), #eq(x_2, y_2)) , #eq(::(x_1, x_2), nil()) -> #false() , #eq(nil(), ::(y_1, y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(y)) -> #false() , #eq(#0(), #neg(y)) -> #false() , #eq(#0(), #pos(y)) -> #false() , #eq(#s(x), #0()) -> #false() , #eq(#s(x), #s(y)) -> #eq(x, y) , #eq(#neg(x), #0()) -> #false() , #eq(#neg(x), #neg(y)) -> #eq(x, y) , #eq(#neg(x), #pos(y)) -> #false() , #eq(#pos(x), #0()) -> #false() , #eq(#pos(x), #neg(y)) -> #false() , #eq(#pos(x), #pos(y)) -> #eq(x, y) , filter(p, ::(x, xs)) -> filter'(#equal(#mod(x, p), #0()), x, filter(p, xs)) , filter(p, nil()) -> nil() , #mod(x, y) -> #sub(x, #mult(y, #div(x, y))) , filter'(#true(), x, xs) -> xs , filter'(#false(), x, xs) -> ::(x, xs) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(y)) -> #0() , #div(#0(), #pos(y)) -> #0() , #div(#neg(x), #0()) -> #divByZero() , #div(#neg(x), #neg(y)) -> #positive(#natdiv(x, y)) , #div(#neg(x), #pos(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #0()) -> #divByZero() , #div(#pos(x), #neg(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #pos(y)) -> #positive(#natdiv(x, y)) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(y)) -> #0() , #mult(#0(), #pos(y)) -> #0() , #mult(#neg(x), #0()) -> #0() , #mult(#neg(x), #neg(y)) -> #pos(#natmult(x, y)) , #mult(#neg(x), #pos(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #0()) -> #0() , #mult(#pos(x), #neg(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #pos(y)) -> #pos(#natmult(x, y)) , #sub(x, #0()) -> x , #sub(x, #neg(y)) -> #add(x, #pos(y)) , #sub(x, #pos(y)) -> #add(x, #neg(y)) , #add(#0(), y) -> y , #add(#neg(#s(#0())), y) -> #pred(y) , #add(#neg(#s(#s(x))), y) -> #pred(#add(#pos(#s(x)), y)) , #add(#pos(#s(#0())), y) -> #succ(y) , #add(#pos(#s(#s(x))), y) -> #succ(#add(#pos(#s(x)), y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(x))) -> #neg(#s(#s(x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) , #succ(#pos(#s(x))) -> #pos(#s(#s(x))) , #and(#true(), #true()) -> #true() , #and(#true(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#false(), #false()) -> #false() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(y)) -> #0() , #natdiv(#s(x), #0()) -> #divByZero() , #natdiv(#s(x), #s(y)) -> #natdiv'(#divsub(x, y), #s(y)) , #natdiv(#underflow(), y) -> #0() , #positive(#0()) -> #0() , #positive(#s(x)) -> #pos(#s(x)) , #positive(#neg(x)) -> #neg(x) , #positive(#pos(x)) -> #pos(x) , #negative(#0()) -> #0() , #negative(#s(x)) -> #neg(#s(x)) , #negative(#neg(x)) -> #pos(x) , #negative(#pos(x)) -> #neg(x) , #natmult(#0(), y) -> #0() , #natmult(#s(x), y) -> #natadd(y, #natmult(x, y)) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(y)) -> #underflow() , #divsub(#s(x), #0()) -> #s(x) , #divsub(#s(x), #s(y)) -> #divsub(x, y) , #natdiv'(#0(), y) -> #s(#0()) , #natdiv'(#s(x), y) -> #s(#natdiv(#s(x), y)) , #natdiv'(#underflow(), y) -> #0() , #natadd(#0(), y) -> y , #natadd(#s(x), y) -> #s(#natadd(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { eratos^#(::(x, xs)) -> eratos^#(filter(x, xs)) , eratos^#(::(x, xs)) -> filter^#(x, xs) , filter^#(p, ::(x, xs)) -> c_2(filter^#(p, xs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Weak Trs: { #equal(x, y) -> #eq(x, y) , #eq(::(x_1, x_2), ::(y_1, y_2)) -> #and(#eq(x_1, y_1), #eq(x_2, y_2)) , #eq(::(x_1, x_2), nil()) -> #false() , #eq(nil(), ::(y_1, y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(y)) -> #false() , #eq(#0(), #neg(y)) -> #false() , #eq(#0(), #pos(y)) -> #false() , #eq(#s(x), #0()) -> #false() , #eq(#s(x), #s(y)) -> #eq(x, y) , #eq(#neg(x), #0()) -> #false() , #eq(#neg(x), #neg(y)) -> #eq(x, y) , #eq(#neg(x), #pos(y)) -> #false() , #eq(#pos(x), #0()) -> #false() , #eq(#pos(x), #neg(y)) -> #false() , #eq(#pos(x), #pos(y)) -> #eq(x, y) , filter(p, ::(x, xs)) -> filter'(#equal(#mod(x, p), #0()), x, filter(p, xs)) , filter(p, nil()) -> nil() , #mod(x, y) -> #sub(x, #mult(y, #div(x, y))) , filter'(#true(), x, xs) -> xs , filter'(#false(), x, xs) -> ::(x, xs) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(y)) -> #0() , #div(#0(), #pos(y)) -> #0() , #div(#neg(x), #0()) -> #divByZero() , #div(#neg(x), #neg(y)) -> #positive(#natdiv(x, y)) , #div(#neg(x), #pos(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #0()) -> #divByZero() , #div(#pos(x), #neg(y)) -> #negative(#natdiv(x, y)) , #div(#pos(x), #pos(y)) -> #positive(#natdiv(x, y)) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(y)) -> #0() , #mult(#0(), #pos(y)) -> #0() , #mult(#neg(x), #0()) -> #0() , #mult(#neg(x), #neg(y)) -> #pos(#natmult(x, y)) , #mult(#neg(x), #pos(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #0()) -> #0() , #mult(#pos(x), #neg(y)) -> #neg(#natmult(x, y)) , #mult(#pos(x), #pos(y)) -> #pos(#natmult(x, y)) , #sub(x, #0()) -> x , #sub(x, #neg(y)) -> #add(x, #pos(y)) , #sub(x, #pos(y)) -> #add(x, #neg(y)) , #add(#0(), y) -> y , #add(#neg(#s(#0())), y) -> #pred(y) , #add(#neg(#s(#s(x))), y) -> #pred(#add(#pos(#s(x)), y)) , #add(#pos(#s(#0())), y) -> #succ(y) , #add(#pos(#s(#s(x))), y) -> #succ(#add(#pos(#s(x)), y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(x))) -> #neg(#s(#s(x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(x)))) -> #pos(#s(x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(x)))) -> #neg(#s(x)) , #succ(#pos(#s(x))) -> #pos(#s(#s(x))) , #and(#true(), #true()) -> #true() , #and(#true(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#false(), #false()) -> #false() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(y)) -> #0() , #natdiv(#s(x), #0()) -> #divByZero() , #natdiv(#s(x), #s(y)) -> #natdiv'(#divsub(x, y), #s(y)) , #natdiv(#underflow(), y) -> #0() , #positive(#0()) -> #0() , #positive(#s(x)) -> #pos(#s(x)) , #positive(#neg(x)) -> #neg(x) , #positive(#pos(x)) -> #pos(x) , #negative(#0()) -> #0() , #negative(#s(x)) -> #neg(#s(x)) , #negative(#neg(x)) -> #pos(x) , #negative(#pos(x)) -> #neg(x) , #natmult(#0(), y) -> #0() , #natmult(#s(x), y) -> #natadd(y, #natmult(x, y)) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(y)) -> #underflow() , #divsub(#s(x), #0()) -> #s(x) , #divsub(#s(x), #s(y)) -> #divsub(x, y) , #natdiv'(#0(), y) -> #s(#0()) , #natdiv'(#s(x), y) -> #s(#natdiv(#s(x), y)) , #natdiv'(#underflow(), y) -> #0() , #natadd(#0(), y) -> y , #natadd(#s(x), y) -> #s(#natadd(x, y)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Wall-time: 31.61699s CPU-time: 372.978299s Hurray, we answered YES(O(1),O(n^2))